Implementing a propositional logic resolution theorem prover. Extending the scheme by allowing a quasi-first-order re-write scheme as a preprocessor. Exercising the theorem prover on the wumpus-world environment.
Your program should read a background knowledge file, containing quasi-first-order knowledge (of the type required for wumpus world). The program should be capable of re-writing the rules into a set of propositional sentences, by instantiating all variables accordingly. Provide your own format, for your convenience and ease of parsing. For example, an input file might be (LISP or SCHEME style):
(VAR i 1 2) ; i is a variable that gets values 1 or 2 (VAR j 2 3) ; j is a variable that gets values 2 or 3 (VAR k 1 2 3) ; k is a variable that gets values 1 or 2 or 3 (or (not (S i j)) (W i j) (W (+ i 1) j)) ; i.e. Sij implies Wij or W(i+1)j (or (not (B i k)) (P i k) (P (+ i 1) k)) S22
The above is expanded by allowing the variables to range over the specified domains, and the result should be the set of sentences (propositional KB):
not S12 or W12 or W22 not S13 or W13 or W23 not S22 or W22 or W32 not S23 or W23 or W33 not B11 or P11 or P21 not B12 or P12 or P22 not B13 or P13 or P23 not B21 or P21 or P31 not B22 or P22 or P32 not B23 or P23 or P33 S22
Your program (both for debugging purposes and for grading purposes) should allow the option for printing out this intermediate result, but only upon request by the user. In addition, the program should now store the result, either internally or as a file, as its propositional KB.
After the above is done, the program should allow the user 2 options:
An item added becomes part of the internally stored KB (but no need to change the original quasi-first-order file). When a query proposition is received, your program should try to use a refutation proof (by resolution only) of the proposition, and of its negation, and report the results. You should have the option to print the set of resolution steps used in the proof. Remember that clauses generated during the proof process should be removed after responding to a query!
Finally, write a quasi-first-order KB for a 4 by 4 wumpus world, and show how your program is used to find location of wumpus, pits, etc.
To sum up, you need to implement 4 elements:
Note that your program should really implement resolution theorem proving, and NOT be specific to wumpus world!
Since satisfiability of propositional sentences is NP-hard, and we do not wish your program to run forever, we will give up on completeness. Use one or more of the following methods to make sure your reasoning algorithm returns in reasonable time:
You need to turn in:
Deadline: May 4, 2003.