COMP316A: Artificial Intelligence Techniques and Applications

- Assignment 3: Logic -

Your job in this assignment is to implement two automatic proving methods for propositional logic, based on a text file that holds a knowledge base as a list of clauses and a query given as another command-line argument. Your job is to implement both backward chaining and the resolution method. In the case of backward chaining, you can assume that the clauses in the knowledge base are definite Horn clauses, because this is what backward chaining requires. In the case of the resolution method, the clauses can be arbitrary disjunctions of literals.

1. First, you need to write some code that reads a list of clauses (i.e. the knowledge base) from a file and stores them in an appropriate data structure. Each line in the file contains one clause, with literals separated by a space. A literal is either an uppercase letter (propositional symbol), or an uppercase letter with a minus in front of it (negated propositional symbol). Here is an example with three clauses (the last one being a fact):
   

   -A B
-B -A C
A


    

2. Then, write a program that takes the name of a file holding a knowledge base and a propositional symbol as command-line arguments and runs backward chaining to check whether the proposition is entailed by the knowledge base. For example, assume that the knowledge base consists of the three lines shown above and is stored in a file called KB, and that the query proposition is B. Then, given the command-line:
   

   java BackwardChaining KB B

   your program must output Knowledge base entails proposition. If the knowledge base does not entail the proposition it must output Knowledge base does not entail proposition. As mentioned above, you can assume that the knowledge base consists of definite Horn clauses, i.e. clauses that have exactly one positive literal (because this is what backward chaining requires). Furthermore, you can assume that the last literal in the definition of a clause is always the positive literal.

    

3. The third part is to implement the resolution proof method. Write a program that accepts a knowledge base in the same format as above (but this time not restricted to Horn clauses) and a disjunction of literals as a second argument at the command-line, and outputs either Contradiction found or No contradiction found. For example, the command-line:
   

   java Resolution KB "-A -C"

   must give the output Contradiction found for the knowledge base given above (which means the negation of the given clause, A /\ C, is entailed by the knowledge base).

Other Information

Value: 11% of the final grade
Due date: Wednesday, 9 April, midday

No extensions will be granted except for sound, documented, medical reasons.