Description
The goal of this assignment is to implement a Resolution theorem prover that can be used to make inferences from a propositional knowledge base (KB), using proof by negation. Specifically, given a set of sentences KB, determine whether a query q is entailed, KB |= q? You will write a program that can read in a file that contains a set of clauses in Conjunctive Normal Form (CNF). This file will consist of the initial KB and the negation of the desired query (q). Your program must then perform resolution until either you derive the empty clause (success; entailed) or run out of resolutions (failure, q not entailed). You will apply this program for automated reasoning to Sammy’s Sport Shop and prove that the middle box must contain white tennis balls. We will test your program on other propositional reasoning tasks too, so your program must be able to accept any file in the format discussed below as input. Sammy’s Sport Shop You are the proprietor of Sammy’s Sport Shop. You have just received a shipment of three boxes filled with tennis balls. One box contains only yellow tennis balls, one box contains only white tennis balls, and one contains both yellow and white tennis balls. You would like to stock the tennis balls in appropriate places on your shelves. Unfortunately, the boxes have been labeled incorrectly; the manufacturer tells you that you have exactly one box of each, but that each box is definitely labeled wrong. One ball is drawn from each box and observed (assumed to be correct). Given the initial (incorrect) labeling of the boxes above, and the three observations, use Propositional Logic to derive the correct labeling of the middle box. Use propositional symbols in the following form: O1Y means a yellow ball was drawn (observed) from box 1, L1W means box 1 was initially labeled white, and C1B means box 1 actually contains both types of tennis balls. Using these symbols, write propositional rules that capture the implications of what different observations or labels mean, as well as constraints inherent in this problem (e.g. all boxes have different contents) Do it in a complete and general way (writing down all the rules and constraints for this domain, not just the ones needed to make the specific inference about the middle box). Do not include derived knowledge that depends on the particular labeling of this instance shown above. Think of this knowledge base as a ‘basis set’ that could be used make inferences from any way the boxes could be labeled. 10/19/2015 1:51 PM Finally, add the facts describing this particular situation to the knowledge base: {O1Y, O2W, O3Y, L1W, L2Y, L3B} Show that box 2 must contain white balls (C2B) using the Resolution Refutation proof procedure. Part of this assignment is writing out the propositional knowledge base for this problem that captures all the knowledge, and converting it to CNF as input for your theorem prover program. Implementation The overall program has 3 parts: initialization, the main loop that does resolution, and postprocessing. The initialization reads in an input file from the command line and creates an internal list of clauses. The main loop is a search process that generates new clauses and uses a queue, as described below. Finally, if the empty clause is found, you will want to print out the proof tree as a post-processing step, to make the reasoning process more comprehensible. The input file format is defined to have one clause on each line. A clause is just a list of literals separated by white space. You do not need to include the disjunction symbols (‘v’), since all the connectives in a clause are assumed to be OR’s by default in CNF. For convenience, you can also skip empty lines and lines starting with a ‘#’ (e.g. comments in your KB file). Here is an example. A set of clauses { A v B v C, B v D, A} can be written in this file format as follows: A B -C -B D # the following singleton clause is a ‘fact’ A This file format is defined to make clauses easy to “parse.” You could represent them internally by using a class to represent a Clause, but there is not much more to it than a list of strings (the literals, positive and negative propositions). The convention we will use is that negative literals are just strings with a ‘-‘ prefixed as the first character. (In my implementation, I also keep track of the indexes of the parent clauses that were used by resolution to generate new clauses. This is useful for doing the traceback of the proof at the end.) In the main loop, the list of input clauses will be augmented by using resolution to generate new clauses. The main loop of the program carries out this process like a Queue-based Search. The queue stores candidate pairs of clauses (for which you could have a class called ResPair, or something like that) that can be resolved but have not been processed yet. The queue gets initialized with all pairs (i,j) where 0<=i<j R v S , A -> -R , A, P, Q } Suppose we want to show the KB |= S by Resolution Refutation. First, negate the query and add it to the KB. Then we convert the KB to CNF: KB = { -P v Q v R v S , -A v -R , A, P, Q, -S } These clauses can be written in a file using the format described above: example1.kb: ———— # P ^ Q -> R v S converted to CNF -P -Q R S -A -R A P Q # negation of the query, S -S We run the resolution program on this file, which succeeds in deriving the empty clause (after generating several intermediate clauses by resolution) and then prints out the proof tree. Note that clauses that have been previously seen are detected and discarded, which is why some resolvents (generated clauses) below are dropped and not added to the clause database. 10/19/2015 1:51 PM 212 sun.cs.tamu.edu> python reso.py example1.kb 0: -P v -Q v R v S 1: -A v -R 2: A 3: P 4: Q 5: -S iteration 1, queue size 5, resolution on 1 and 2 resolving -A v -R and A 6: -R generated from 1 and 2 iteration 2, queue size 5, resolution on 0 and 4 resolving -P v -Q v R v S and Q 7: -P v R v S generated from 0 and 4 iteration 3, queue size 8, resolution on 7 and 3 resolving -P v R v S and P 8: R v S generated from 7 and 3 iteration 4, queue size 10, resolution on 8 and 5 resolving R v S and -S 9: R generated from 8 and 5 iteration 5, queue size 11, resolution on 9 and 6 resolving R and -R success! empty clause found 10: [] [9,6] 9: R [8,5] 8: R v S [7,3] 7: -P v R v S [0,4] 0: -P v -Q v R v S [input] 4: Q [input] 3: P [input] 5: -S [input] 6: -R [1,2] 1: -A v -R [input] 2: A [input] What to Turn in: Submit your code for testing using the web-based CSCE turnin facility, which is described here: https://wiki.cse.tamu.edu/index.php/Turning_in_Assignments_on_CSNet (you might have to be inside the TAMU firewall to access this) Include a document that details how to compile and run your code. Provide a brief overview of how your program works, including significant data structures and algorithmic details (such as how you implemented the heuristic or visited list), and how they might impact the performance of your program. Provide a text document with your knowledge base (propositional rules) for Sammy’s Sport Shop. Provide the input file for Sammy’s Sport Shop, with all the rules and facts converted to CNF. Give a transcript of your program solving Sammy’s Sport Shop, showing a trace of all the resolution steps and a trace of the proof when the empty clause is found. Report the total number of resolutions (iterations of the main loop) and max queue size. (You might also want to optionally include a trace of another inference example, such as example1.kb above, or perhaps ‘safe22’ in the Wumpus World.)
