COSC 574 Project 1

COSC 574: Automated Reasoning

Project 1
Spring 2016

First deliverable (p1a, 10%): F 2/5 @ 11:59 PM
Second deliverable (p1b, 10%): W 2/17 @ 11:59 PM
Final deliverable (p1, 80%): Su 2/28 @ 11:59 PM
20 points

In this project, you will implement a theorem prover for first-order logic using linear resolution.

For this and subsequent projects, you must implement your program using a language such as ANSI C++, Java, Python, or Ruby. Your code must be well-structured and well-organized and follow object-oriented design principles. Your code must compile and run on cs-class. If you want to use some other language, check with me first.

For this and subsequent projects, you must implement your program using the standard libraries the language provides. If you want to use external libraries or something non-standard, check with me first.

Finally, for this and subsequent projects, it must be easy for me to build and run your project. Make sure you include instructions in a README file that describes exactly how to build and run your project. If you use Java, do not use packages. If you use C++, provide a Makefile. Ultimately, I should be able to drop in your project's directory, compile it, if necessary, and execute it.

I have divided the project into three deliverables:

Write a program and the classes and methods necessary to read, parse, store, and output first-order well-formed formulas (wffs). Formulas must be stored internally as expression trees.
The following grammar specifies the syntax for wffs.
```
formula ::= '(' predicate-name argument-list ')'
          | '(' 'not' formula ')'
          | '(' 'or' formula formula ')'
          | '(' 'and' formula formula ')'
          | '(' 'cond' formula formula ')'
          | '(' 'forall' variable formula ')'
          | '(' 'exists' variable formula ')'

predicate-name ::= identifier

argument-list ::= argument arguments

arguments ::= argument arguments | ε

argument ::= function-or-constant-or-variable

function-or-constant-or-variable ::= function | constant | variable

function ::= '(' function-name argument-list ')'

function-name ::= identifier

identifier ::= letter letters-and-digits

constant ::= constant-letter letters-and-digits
           | variable-letter letter letters-and-digits

constant-letter ::= 'a'..'t' | 'A'..'Z'

variable ::= variable-letter | variable-letter digits

variable-letter ::= 'u'..'z'

digits ::= digit digits | ε

letters-and-digits ::= letter-or-digit letters-and-digits | ε

letter-or-digit ::= letter | digit

letter ::= 'a'..'z' | 'A'..'Z'

digit ::= '0'..'9'
```
Examples of wffs written in this syntax are:
- Jack owns a dog
- All cats are animals
- No animal lover kills an animal
To support development, I have created files for two proofs that appear in Russell and Norvig, the proof that Curiosity did not kill the cat and the proof that Colonel West is a criminal. 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.
For the first deliverable, you must produce a single executable that takes a file name as a command-line argument. For each formula in the file, the program must parse it, store it as an expression tree, and print the string representation of the expression tree to the console.
In addition to the Curiosity and West proofs, you must find two additional proofs from reputable sources consisting of at least four clauses and three predicates. Naturally, I will test your program on my own set of proofs.
Include with your submission the proof files and a transcript of your program's execution on the four files.
In the header comments in at least the main file of your project, provide the following information:
```
//
// Name
// E-mail Address
// Platform: Windows, OS X, Linux, etc.
// Language/Environment: gcc, g++, java, ruby, python
//
// 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 program for grading, create a zip file of the directory containing only your project's source, proof files, transcript, and build instructions, and upload it to Blackboard.

Implement the routines to convert wffs to clausal form. For the second deliverable, you must produce a single executable that takes a file name as a command-line argument. For the formulas in the file, the program must read and store them, print them to the console, convert them to clausal form, store them as expression trees, and print them to the console. Include with your submission the proof files and a transcript of your program's execution on the four files.
When you are ready to submit your program for grading, create a zip file of the directory containing only your project's source, proof files, transcript, and build instructions, and upload it to Blackboard.

Implement the routines to required to conduct resolution proofs using linear resolution.

For the final deliverable, you must produce a single executable that takes a file name as a command-line argument. The program should read the formulas in the file and conduct a resolution proof using linear resolution. The program should print the formulas, the converted clauses, and a trace of the proof consisting of each clause C_i its resolvents from Δ and S. Finally, it should print a message indicating whether it was able to derive the conclusion from the premises. Include with your submission the proof files and a transcript of your program's execution on the four files.

When you are ready to submit your program for grading, create a zip file of the directory containing only your project's source, proof files, transcript, and build instructions, and upload it to Blackboard.