Project 2
Fall 2022
Due: F 10/7 @ 5 PM ET
9 points
For this project, you will implement a resolution theorem prover for propositional logic.
I have divided the project into three phases:
The following grammar specifies the syntax for wffs.
formula ::= '(' proposition ')' | '(' 'not' formula-or-proposition ')' | '(' 'or' formula-or-proposition formula-or-proposition ')' | '(' 'and' formula-or-proposition formula-or-proposition ')' | '(' 'cond' formula-or-proposition formula-or-proposition ')' formula-or-proposition ::= formula | proposition proposition ::= letter letters-and-digits letters-and-digits ::= letter-or-digit letters-and-digits | \epsilon letter-or-digit ::= letter | digit letter ::= 'a'..'z' | 'A'..'Z' digit ::= '0'..'9'
Examples of wffs written in this syntax are:
To support development, I put some starter code on cs-class. To get started, log on to cs-class and copy over the following zip file:
cs-class-1% cd cs-class-1% cp ~maloofm/cosc570/p2.zip ./ cs-class-1% unzip p2.zipThere is also a copy on Canvas. In the p2 directory, you will find a class implementation for Tokenizer and a partial implementation for Formula. The Tokenizer class demonstrates how to configure Scanner to tokenize propositional logic formulae. The directory also contains files for the two proofs we discussed in lecture, Example 1 and the proof that beggars do not ride horses. As you can see in the files, comments begin with a forward slash, formulas begin with a left parenthesis, and both are confined to a single physical line. By convention, the last formula in the file is the conclusion.
In addition to the these proofs, you must find two additional proofs from reputable sources consisting of at least three formulas and three propositions. Include these proof files with your submission to Autolab. Naturally, I will test your program on my own set of proofs.
For this first phase, you must implement the class Formula with the methods
When you submit to Autolab, the autograder will call these three methods. Naturally, you will need to implement additional methods.
clause ::= '{' literals '}' literals ::= literal literals-comma-separated | \epsilon literals-comma-separated ::= ',' literal literals-comma-separated | \epsilon literal ::= proposition | '(' 'not' proposition ')'
You must implement
The transformations must preserve the order of literals. For example, (cond p q) should be written in CNF as ((not p) q), not as (q (not p)); (cond p q) should be written as the clause {(not p), q}, not as {q, (not p)}.
You must implement
Include with your submission the proof files and a transcript of your program's execution for the four proofs. The transcript should be a plain ASCII file named README. In a file named HONOR, include the following statement:
In accordance with the class policies and Georgetown's Honor Code, I certify that, with the exceptions of the class resources and those items noted below, I have neither given nor received any assistance on this project. Name NetID
When you are ready to submit your project for grading, put your source files, Makefile, proof files, transcript, and honor statement in a zip file named submit.zip. Upload the zip file to Autolab using the assignment p2. Make sure you remove all debugging output before submitting.
Copyright © 2022 Mark Maloof. All Rights Reserved. This material may not be published, broadcast, rewritten, or redistributed.