tailieunhanh - Artificial Intelligence - Lecturer 11: Inference in First Order Logic

Herbrand showed that there is a procedure to demonstrate the unsatisfiability of a unsatisfiable set of sentences. Robinson propose the Resolution procedure. The law says that it is a crime for an American to sell weapons to hostile nations. | 5 18 2014 Artificial Intelligence For HEDSPI Project Lecturer 11 - Inference in First Order Logic Lecturers Dr. Le Thanh Huong Dr. Tran Duc Khanh Dr. Hai V. Pham HUST First Order Logic Syntax Semantic Inference Resolution 1 5 18 2014 Inference in FOL Difficulties Quantifiers Infinite sets of terms Infinite sets of sentences Examples x A Greedy x Evil x Infinite set of instances King Bill A Greedy Bill Evil Bill King FatherOf Bill A Greedy FatherOf Bill Evil FatherOf Bill Robinson s Resolution Herbrand s Theorem 1930 A set of sentences S is unsatisfiable if and only there exists a finite subset Sg of the set of all ground instances Gr S which is unsatisfiabe Herbrand showed that there is a procedure to demonstrate the unsatisfiability of a unsatisfiable set of sentences Robinson propose the Resolution procedure 1950 2 5 18 2014 Idea of Resolution Refutation-based procedure S1 A if and only if S u lA is unsatisfible Resolution procedure Transform S u A into a set of clauses Apply Resolution rule to find a the empty clause contradiction If the empty clause is found Conclude S 1 A Otherwise No conclusion Clause A clause is a disjunction of literals . has the form P V P2 V. V Pn Pi R Example P x V Q x a V R b P y V Q b y V R y The empty clause corresponds to a contradiction Any sentence can be transformed to an equi-satisfiable set of clauses