COSC-574: Automated Reasoning

Project 2
Fall 2019

First deliverable (p1a, 5 points): F 10/11 @ 5 PM
Second deliverable (p1b, 5 points): F 10/25 @ 5 PM
Final deliverable (p1c, 20 points): F 11/15 @ 5 PM
30 points total

I have divided the project into three deliverables:

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

    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. Please do not change the names of these files since the autograder uses them.

    In addition to the Curiosity and West proofs, you must find two additional proofs from reputable sources consisting of at least four formulas and three predicates. Naturally, I will test your program on my own set of proofs.

    For the first deliverable, Main.main in Main.java should take 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.

    You must implement the class Formula with the methods

    public Formula();
    public void set( String s );
    public String toString();
    
    In addition to calling Main.main, the autograder will call these three methods.

    Include with your submission the two 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 program for grading, create a zip file named submit.zip containing your project's source files, proof files, transcript, and honor statement. Upload the zip file to Autolab using the assignment p1a.
  2. Implement the routines to convert wffs to clausal form. For the second deliverable, Main.main must take 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.

    You must implement

    To standardize variables apart, use the prefix qv for &ldqou;quantified variable” and add to it a counter for each quantified variable in the formula. The prefix for Skolem constants must be sc. The prefix for Skolem functions must be sf.

    When you are ready to submit your project for grading, put your source files, proof files, transcript, and honor statement in a zip file named submit.zip. Upload the zip file to Autolab using the assignment p1b.

  3. 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 proof using linear resolution. The program should print the formulas, the converted clauses, and a trace of the proof consisting of each clause Ci its resolvents from Δ and S. Finally, it should print a message indicating whether it was able to derive the conclusion from the premises.

    You must also implement

    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 project for grading, put your source files, proof files, transcript, and honor statement in a zip file named submit.zip. Upload the zip file to Autolab using the assignment p1c.

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