COSC-270: Artificial Intelligence

Project 2
Fall 2019

Due: F 10/25 @ 5 PM
10 points

For this project, you will implement a resolution theorem prover for propositional logic.

I have divided the project into three phases:

1. For the first phase, write the classes and methods necessary to read, parse, store, and output propositional well-formed formulas (wffs). Formulas must be stored internally as expression trees.

   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:

   • Wishes are horses provided that horses cannot fly.
   • \( \neg\mbox{HF} \rightarrow \mbox{W} \)
   • (cond (not hf) w)
   • If it is not the case that both beggars ride and wishes are nonequine, then horses can fly.
   • \( \neg (\mbox{BRD} \; \& \; \neg\mbox{W}) \rightarrow \mbox{HF} \)
   • (cond (not (and brd (not w))) hf)

   To support development, I have created files for two proofs that we discussed in lecture, the proof Example 1 and the proof that beggers do not ride horses. As you can see, 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. Naturally, I will test your program on my own set of proofs.

   For this phase, you must implement the class Formula with the methods

   public Formula();
   public void set( String s );
   public String toString();
   

   When you submit to Autolab, the autograder will call these three methods. Naturally, you're free to implement additional methods.

2. For the second phase, implement the routines to convert wffs to clausal form. Clauses must be stored internally as expression trees or more precisely a linked list of literals. The following grammar specifies the syntax for clauses.

   clause ::= '{' literals '}'
   
   literals ::= literal literals-comma-separated
   
   literals-comma-separated ::= ',' literal literals-comma-separated | \epsilon
   
   literal ::= proposition
            | '(' 'not' proposition ')'
   

   You must implement

   • public void Formula.cnf(), which converts a formula to conjunctive normal form
   • public class Clauses, which simply extends ArrayList<Clause>
   • public Clauses Formula.getClauses(), which converts a formula to clausal form and returns the resulting clauses
   • public String Clause toString(), which returns the string representation of the clause
3. Finally, implement the routines to required to conduct proofs using resolution. For this final phase, you must implement Main.java so it takes a file name as a command-line argument. Main.main read the formulas in the file, negate the conclusion, convert the formulas to clausal form, and conduct a proof using resolution. The program should print the formulas, the converted clauses, a trace of the proof consisting of the successful resolutions, and a message indicating whether it was possible to derive the conclusion from the premises.

   You must implement

   • public Clause().
   • public void Clause.set( String ), which sets the Clause to the clause that the specified String represents.
   • public Clause Clause.resolve( Clause clause ) throws FailedToResolveException, which resolves the clause in Clause with the specified Clause clause and returns the resolvent. If the two clauses do not resolve, then the method should throw FailedToResolveException, which you should derive from RuntimeException
   • public static boolean Resolution.prove( String filename ), which returns true if the conclusion follows from the premises and returns false otherwise.

   Include with your submission the proof files and a transcript of your program's execution for the four proofs. In a file named HONOR, include the following statement:

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

   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.

Plan B

Copyright © 2019 Mark Maloof. All Rights Reserved. This material may not be published, broadcast, rewritten, or redistributed.