First Order Logic
First Order Logic
First Order Logic
First-Order Logic
Chapter 7.4─7.8, 8.1─8.3, 8.5
Some material adopted from notes by Andreas Geyer-Schulz and Chuck Dyer
Logic roadmap overview
• Propositional logic (review)
• Problems with propositional logic
• First-order logic (review)
– Properties, relations, functions, quantifiers, …
– Terms, sentences, wffs, axioms, theories, proofs, …
• Extensions to first-order logic
• Logical agents
– Reflex agents
– Representing change: situation calculus, frame problem
– Preferences on actions
– Goal-based agents
Disclaimer
P=true, Q=false
✔ P=false, Q=true
A B A→B OK?
True True True
True False False
False True True
False False True
Resolution
• Resolution is a valid inference rule producing a new
clause implied by two clauses containing
complementary literals
– A literal is an atomic symbol or its negation, i.e., P, ~P
• Amazingly, this is the only interference rule you need
to build a sound and complete theorem prover
– Based on proof by contradiction and usually called
resolution refutation
• The resolution rule was discovered by Alan Robinson
(CS, U. of Syracuse) in the mid 60s
Resolution
• A KB is actually a set of sentences all of which are
true, i.e., a conjunction of sentences.
• To use resolution, put KB into conjunctive normal
form (CNF), where each sentence written as a disjunc-
tion of (one or more) literals
Tautologies
Example (AB)↔(~AB)
• KB: [PQ , QRS] (A(BC)) ↔(AB)(AC)
• KB in CNF: [~PQ , ~QR , ~QS]
• Resolve KB(1) and KB(2) producing: ~PR (i.e., PR)
• Resolve KB(1) and KB(3) producing: ~PS (i.e., PS)
• New KB: [~PQ , ~Q~R~S , ~PR , ~PS]
Soundness of the
resolution inference rule