Description

CENG462
Artificial Intelligence
Homework 2 (v2)

1 Objectives
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)’])
5 Regulations
1. Programming Language: You must code your program in Python 3. Your submission will be tested in inek machines. So make sure that it can be executed on them as below.
[ GCC 8.4.0] on linux
>>> import e1234567_hw2
>>> e1234567_hw2 . theorem_prover ( . . . )
2. Implementation: You have to code your program by only using the functions in standard module of python. Namely, you cannot import any module in your program.
5. Discussion: You must follow the OdtuClass for discussions and possible updates on a daily basis.
6 Submission
Submission will be done via OdtuClass system. You should upload a single python file named in the format <your-student-id> hw2.py (i.e. e1234567 hw2.py).
2