(Message 83) From: HELEN HPS (on ERCC DEC-10) Date: Wednesday, 30-Jan-85 22:59:37-GMT To: ecmi04@2972,Pain@EDXA Via: uk.ac.edinburgh.edxa ; (to uk.ac.edinburgh.emas) 30 Jan 85 23:01:21 gmt Msg ID: <132017-752-421@EDXA> -------- AI1 PROLOG PROJECTS: QUIP - A RESOLUTION THEOREM PROVER AI1 PROLOG PROJECTS: QUIP - A RESOLUTION THEOREM PROVER AI1 PROLOG PROJECTS: QUIP - A RESOLUTION THEOREM PROVER Dave Plummer 30 January 1985 Quip is a resolution theorem prover written in PROLOG. In this project you are asked to investigate and understand the code, and to make some extensions to the program. Look at the file: 'ecmi04.quip' At the front of the file is some information about what the program does and how it is used. Decide what the program does and how it does it. Construct some examples to check that you understand the program. When you think that you understand how the program works do the following: 1. Write documentation for the program, a paragraph for each of the procedures in the program, describing what each procedure does, and how it does it. 2. Provide at least 3 example traces of the program in the project report. Choose at least two of the extensions from the list below and make these extensions to the program. For each, include in your project report: i. a description of the extension to the program; ii. a listing of the program to indicate the changes made; iii. a number of examples to illustrate the extension; iv. any relevant discussion of the problem; how you solved it, how else you might have solved it, where it fails and why, etc. _______ __________ Program_Extensions 1. Insert commands into the program which prompt the user of the program to input clauses. 2. Insert commands to show the user the clauses that are generated while the proof progresses. Eg: "Resolving 'a v b' with '-a v c' to get 'b v c'." "Resolving 'b v c' with '-c' to get 'b'." Show 6 examples of the program running with this extension made. 2 3. Take 3 of the above examples and reorder the hypotheses, note the changes in the steps of the proof and explain why the number of steps taken to perform a proof may vary. 4. Alter the program to enable a user to state the hypotheses in the more natural notation: "avb." for "[a,b]." [Hint: the PROLOG procedure name/2 takes an atom and turns it into a list of the code numbers of the letters in the word]. 5. Think about how the program might be extended to take sentences of the full propositional calculus and turn them into clauses by using the rules below which rewrite a sentences to an equivalent form. Eg: "a v (b & c)" rewrites to "(a v b) & (a v c)". "(a -> b)" rewrites to "-a v b". Discuss how this might be done, even if you don't get as far as doing so. What are the problems? What are the possible methods of solution, which work, which don't, and why? Of these, 1 is the easiest, 2 is moderately easy, 3 and 4 are moderately hard, and 5 is hard. Please provide TWO copies of your project report, including all listings and examples. These should be submitted to Helen Pain, by Monday 22nd April (that is, Monday of week 2 of next term). --------