This assignment aims to assist you to expand your knowledge on First Order Predicate Logic.
2 Problem Definition
In this assignment, you are going to implement a function called theorem prover in python as a theorem prover for First Order Predicate Logic by using Resolution Refutation technique and Linear Input Strategy in the written order of clauses. This function gets two lists of clauses in Conjunctive Normal Form (CNF), namely the list of base clauses and the list of clauses obtained from the negation of the theorem.
Your program has to eliminate
• tautologies
• subsumptions in the case of a resolution.
The function detects whether the theorem is derivable or not. Then, it returns the result as a tuple. First element of this tuple will be “yes” or “no” according to derivability of the theorem. The second element will be list of all resolutions that are processed during the search of proof. Further details about the return value can be seen in the following sections.
3 Specifications
• As Linear Input Strategy indicates, at least one parent must be selected from the initial base set of clauses (the given list of base clauses together with the negation of the theorem) while processing a resolution.
• By the convention we follow in FOPL; variables, predicate and function names start with with a lower case letter, while the names of the constants start with an upper case letter. Note that none of these does not have to be a one-letter name.
1
• In the given clauses; “+” and “!” signs will be used for disjunction and negation respectively.
• Each resolution in the return value must be given in “< clause1 > $ < clause2 > $ < resolvent >” form without using any space character.
• The “empty” string must be used for empty clause in the return value.
4 Sample Function Calls
>>> theorem_prover(["p(A,f(t))", "q(z)+!p(z,f(B))", "!q(y)+r(y)"],["!r(A )"])
(’yes’, [’p(A,f(t))$q(z)+!p(z,f(B))$q(A)’, ’q(A)$!q(y)+r(y)$r(A)’, ’r(A) $!r(A)$empty’])
>>> theorem_prover(["p(A,f(t))", "q(z)+!p(z,f(B))", "q(y)+r(y)"],["!r(A) "])
(’no’, [’p(A,f(t))$q(z)+!p(z,f(B))$q(A)’, ’q(y)+r(y)$!r(A)$q(A)’])
