PROGRAMMING PROJECT #2

Propositional Logic Proof Giver

1. Read:

   Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall R. (1985), Logic: A Computer Approach (New York: McGraw-Hill), Ch. 11: "Sentential Logic: A Method for Producing Proofs", especially the section titled "Suggestions for Computer Implementation" (pp. 246-249).

   • The full textbook is on reserve in UGL.

2. Implement (in your favorite programming language) the Proof Giver program described therein. This will be a program that takes as input an "argument" of propositional logic (called "sentential" logic in the textbook above). A propositional-logic argument has the form:
   PREMISES |- P

   where PREMISES is a set of wffs, called the premises of the argument, and P is a wff, called the conclusion of the argument.

   The output of Proof Giver is a proof of P from PREMISES such that each line of the proof is either:

   • a member of PREMISES or

   • follows from previous lines of the proof by one of the rules of inference of propositional logic, or

   • is a line of a subproof, where each subproof is, recursively, a proof of an argument Q |- R, where Q is a temporary premise justified by one of the rules of inference

   and the last line of the (main) proof is P.

3. To simplify matters, the system of propositional logic for which you should implement Proof Giver will only allow 2 connectives: negation (symbolized by "-") and material conditional (symbolized by ">"). The rules of inference are:
   • -Introduction:
     To derive a wff of the form -P whose main connective is negation (-):
     Begin a subproof with the temporary premise P
     Then derive wffs of the form Q, -Q in that subproof;
     Then infer -P in that subproof
     (And then return -P to the main proof)

   • -Elimination:
     To derive a wff of the form P whose main connective is not negation:
     Begin a subproof with the temporary premise -P
     Then derive wffs of the form Q, -Q in that subproof;
     Then infer P in that subproof
     (And then return P to the main proof)

   • >Introduction:
     To derive a wff of the form (P > Q) whose main connective is the material conditional (>):
     Begin a subproof with the temporary premise P
     Then derive Q in that subproof;
     Then infer (P > Q) in that subproof;
     (And then return (P > Q) to the main proof)

   • >Elimination:
     To derive a wff of the form Q:
     Derive wffs of the form (P > Q) and P
     Then infer Q

   • SEND and RETURN: See Rules for SEND and RETURN

4. 
   There appears to be a bug in the Proof-Giver algorithm for Project 2. The following modification seems to fix the bug: Add a "step 0" to the OBTAIN Q procedure, just before the current step 1:

   ---

   0. If the line containing Q has fewer asterisks than the desired result
      and if Q is of the form (X > Y),
      then insert *SEND,[Q] before DERIVE DR in the task list.

   ---

   Note that unlike other steps, you don't delete or replace the "DERIVE" task; instead, you put a task just before it, but you keep it there.

5. Test your system on the following two problems (which you should also do by hand, whether or not you succeed in implementing Proof Giver):
   • {(A > B), (B > C), (C > D)} |- (A > D)

   • {(A > B), (A > -B) |- -A

6. Your project report should consist of:

   (a) A brief description of reasoning in propositional logic (suitable for a section of the Brachman & Levesque text), including the two proofs above.

   (b) An annotated demo of your implementation of Proof Giver.

   (c) Commented code for your implementation of Proof Giver.

   On Unix, you can format lengthy output with mpage or mpage -2 and then pipe the result to lpr to print it, or save the mpage output to a file with a .ps extension.

7. 
   In addition to the hard copy of your program that should be included with your written report, please use the "submit" facility to submit the program to us. Details on how to use "submit" will be posted to the newsgroup.