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:
   Δ |- α

   where Δ is a set of wffs, called the premises of the argument, and α is a wff, called the conclusion of the argument.

   • If you don't see capital Greek delta and lower-case Greek alpha in the formulas above, then you are using an old browser. In that case, please look at the following webpage instead: Project 2 for older browsers

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

   • a member of Δ 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 β |- γ, where β is a temporary premise justified by one of the rules of inference

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

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 -α whose main connective is negation (-):
     Begin a subproof with the temporary premise α
     Then derive wffs of the form β, -β in that subproof;
     Then infer -α in that subproof
     (And then return -α to the main proof)

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

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

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

   • 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. 
   If you feel that Proof Giver is unable to handle all possible inferences in propositional logic, or if there is some aspect of Proof Giver that you are unable to implement, then please give an analysis or explanation of the "missing" features as part of your report.

7. 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.

8. 
   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.