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 “
*< clause*1*>*$*< clause*2*>*$*< 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)’])

## Reviews

There are no reviews yet.