8a_First_Order_Logic.dvi
COMP9414 First-Order Logic 1
Propositional Logic
� Propositions built from ∧, ∨, ¬,→
� Sound, complete and decidable proof systems (inference procedures)
◮ Natural deduction
◮ Resolution refutation
◮ Prolog for special case of definite clauses
◮ Tableau method
� Limited expressive power
◮ Cannot express ontologies, e.g. AfPak Ontology
� First-Order Logic can express knowledge about objects, properties
and relationships between objects
UNSW ©W. Wobcke et al. 2019–2021
COMP9414: Artificial Intelligence
Lecture 8a: First-Order Logic
Wayne Wobcke
e-mail:w. .au
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 3
Syntax of First-Order Logic
� Constant symbols: a, b, . . . , Mary (objects)
� Variables: x, y, . . .
� Function symbols: f , mother of , sine, . . .
� Predicate symbols: Mother, likes, . . .
� Quantifiers: ∀ (universal); ∃ (existential)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 2
This Lecture
� First-Order Logic
◮ Syntax
◮ Semantics
� Automated Reasoning
◮ Conjunctive Normal Form
◮ First-order resolution and unification
◮ Soundness, completeness, decidability
� Applications
◮ Ontologies
◮ Reasoning About Action
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 5
Converting English into First-Order Logic
� Everyone likes lying on the beach – ∀x likes lying on beach(x)
� Someone likes Fido – ∃x likes(x, Fido)
� No one likes Fido – ¬∃x likes(x, Fido) (or ∀x¬likes(x, Fido))
� Fido doesn’t like everyone – ¬∀x likes(Fido, x)
� All cats are mammals – ∀x(cat(x)→ mammal(x))
� Some mammals are carnivorous – ∃x(mammal(x)∧ carnivorous(x))
� Note: ∀xA(x)⇔¬∃x¬A(x), ∃xA(x)⇔¬∀x¬A(x)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 4
Language of First-Order Logic
� Terms: constants, variables, functions applied to terms (refer to
objects)
◮ e.g. a, f (a), mother of (Mary), . . .
� Atomic formulae: predicates applied to tuples of terms
◮ e.g. likes(Mary, mother of (Mary)), likes(x, a)
� Quantified formulae:
◮ e.g. ∀x likes(x, a), ∃x likes(x, mother of (y))
◮ here the second occurrences of x are bound by the quantifier (∀ in
the first case, ∃ in the second) and y in the second formula is free
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 7
Existential Quantifiers
Some cats are immortal: ∃x(cat(x)∧¬mortal(x))
� ∃xP is (almost) equivalent to the disjunction of instantiations of P
� ∃x(cat(x)∧¬mortal(x))⇔
(cat(Alan)∧¬mortal(Alan))
∨ (cat(Bill)∧¬mortal(Bill))
∨ (cat(Colin)∧¬mortal(Colin))
∨ . . .
. . . only if every object (not only cat) in the domain has a name
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 6
Universal Quantifiers
All men are mortal: ∀x(man(x)→ mortal(x))
� ∀xP is (almost) equivalent to the conjunction of instantiations of P
� ∀x(man(x)→ mortal(x))⇔
(man(Alan)→ mortal(Alan))
∧ (man(Bill)→ mortal(Bill))
∧ (man(Colin)→ mortal(Colin))
∧ . . .
. . . only if every object (not only man) in the domain has a name
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 9
Defining Semantic Properties
Brothers are siblings
∀x∀y(brother(x, y)→ sibling(x, y))
“Sibling” is symmetric
∀x∀y(sibling(x, y)↔ sibling(y, x))
One’s mother is one’s female parent
∀x∀y(mother(x, y)↔ (female(x)∧parent(x, y))
A (first) cousin is a child of a parent’s sibling
∀x∀y(cousin(x, y)↔∃p∃s(parent(p, x)∧ sibling(p, s)∧parent(s, y)))
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 8
Nested Quantifiers
The order of quantification is very important
� Everything likes everything – ∀x∀ylikes(x, y) (or ∀y∀x likes(x, y))
� Something likes something – ∃x∃ylikes(x, y) (or ∃y∃x likes(x, y))
� Everything likes something – ∀x∃ylikes(x, y)
� There is something liked by everything – ∃y∀x likes(x, y)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 11
Scope of Quantifiers
� The scope of a quantifier in a formula A is that subformula B of A of
which that quantifier is the main logical operator
� Variables belong to the innermost quantifier that mentions them
� Examples
◮ Q(x)→∀yP(x, y) – scope of ∀y is ∀yP(x, y)
◮ ∀zP(z)→¬Q(z) – scope of ∀z is ∀zP(z) but not Q(z)
◮ ∃x(P(x)→∀xP(x))
◮ ∀x(P(x)→ Q(x))→ (∀xP(x)→∀xQ(x))
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 10
Scope Ambiguity
� Typical pattern for ∀ and ∃
◮ ∀x(type of (x)→ predicate(x))
◮ ∃x(type of (x)∧predicate(x))
� Every student took an exam
◮ ∀x(student(x)→∃y(exam(y)∧ took(x, y)))
◮ ∃y(exam(y)∧∀x(student(x)→ took(x, y)))
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 13
Towards Resolution for First-Order Logic
� Based on resolution for Propositional Logic
� Extended syntax: allow variables and quantifiers
� Define “clausal form” for first-order logic formulae
� Eliminate quantifiers from clausal forms
� Adapt resolution procedure to cope with variables (unification)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 12
Semantics of First-Order Logic
� An interpretation is required to give semantics to first-order logic. An
interpretation is a non-empty “domain of discourse” (set of objects).
The truth of any formula depends on the interpretation.
� The interpretation defines, for each
constant symbol an object in the domain
function symbol a function from domain tuples to the domain
predicate symbol a relation over the domain (a set of tuples)
� Then by definition
universal quantifier ∀xP(x) is True iff P(a) is True for all
assignments of domain elements a to x
existential quantifier ∃xP(x) is True iff P(a) is True for at least one
assignment of domain element a to x
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 15
Conversion to CNF – Continued
6. Skolemize (replace each existentially quantified variable by a new
term)
◮ ∃xP(x) becomes P(a0) using a Skolem constant a0 since ∃x
occurs at the outermost level
◮ ∀x∃yP(x, y) becomes P(x, f0(x)) using a Skolem function f0
since ∃y occurs within ∀x
7. The formula now has only universal quantifiers and all are at the left
of the formula: drop them
8. Use distribution laws to get CNF and then clausal form
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 14
Conversion to Conjunctive Normal Form
1. Eliminate implications and bi-implications as in propositional case
2. Move negations inward using De Morgan’s laws
◮ plus rewriting ¬∀xP as ∃x¬P and ¬∃xP as ∀x¬P
3. Eliminate double negations
4. Rename bound variables if necessary so each only occurs once
◮ e.g. ∀xP(x)∨∃xQ(x) becomes ∀xP(x)∨∃yQ(y)
5. Use equivalences to move quantifiers to the left
◮ e.g. ∀xP(x)∧Q becomes ∀x(P(x)∧Q) where x is not in Q
◮ e.g. ∀xP(x)∧∃yQ(y) becomes ∀x∃y(P(x)∧Q(y))
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 17
CNF: Example 2
¬∃x∀y∀z((P(y)∨Q(z))→ (P(x)∨Q(x)))
1. ¬∃x∀y∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))
2. ∀x¬∀y∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))
2. ∀x∃y¬∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))
2. ∀x∃y∃z¬(¬(P(y)∨Q(z))∨P(x)∨Q(x))
2. ∀x∃y∃z((P(y)∨Q(z))∧¬(P(x)∨Q(x)))
6. ∀x((P( f (x))∨Q(g(x)))∧¬P(x)∧¬Q(x))
7. (P( f (x))∨Q(g(x))∧¬P(x)∧¬Q(x)
8. {P( f (x))∨Q(g(x)), ¬P(x), ¬Q(x)}
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 16
CNF: Example 1
∀x [∀yP(x, y)→¬∀y(Q(x, y)→ R(x, y))]
1. ∀x [¬∀yP(x, y)∨¬∀y(¬Q(x, y)∨R(x, y))]
2, 3. ∀x [∃y¬P(x, y)∨∃y(Q(x, y)∧¬R(x, y))]
4. ∀x [∃y¬P(x, y)∨∃z(Q(x, z)∧¬R(x, z))]
5. ∀x∃y∃z [¬P(x, y)∨ (Q(x, z)∧¬R(x, z))]
6. ∀x [¬P(x, f (x))∨ (Q(x, g(x))∧¬R(x, g(x)))]
7. ¬P(x, f (x))∨ (Q(x, g(x))∧¬R(x, g(x)))
8. (¬P(x, f (x))∨Q(x, g(x)))∧ (¬P(x, f (x))∨¬R(x, g(x)))
8. {¬P(x, f (x))∨Q(x, g(x)), ¬P(x, f (x))∨¬R(x, g(x))}
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 19
Examples
� {P(x,a),P(b,c)} is not unifiable
� {P( f (x),y),P(a,w)} is not unifiable
� {P(x,c),P(b,c)} is unifiable by {x/b}
� {P( f (x),y),P( f (a),w)} is unifiable by
σ = {x/a,y/w}, τ = {x/a,y/a,w/a}, υ = {x/a,y/b,w/b}
Note that σ is an mgu and τ = σθ where θ = . . .?
� {P(x),P( f (x))} is not unifiable (c.f. occur check!)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 18
Unification
� A unifier of two atomic formulae is a substitution of terms for
variables that makes them identical
◮ Each variable has at most one associated term
◮ Substitutions are applied simultaneously
� Unifier of P(x, f (a), z) and P(z, z, u) : {x/ f (a), z/ f (a), u/ f (a)}
� Substitution σ1 is a more general unifier than a substitution σ2 if for
some substitution τ, σ2 = σ1τ (i.e. σ1 followed by τ)
� Theorem. If two atomic formulae are unifiable, they have a most
general unifier (mgu).
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 21
Applying Resolution Refutation
� Negate query to be proven (resolution is a refutation system)
� Convert knowledge base and negated query into CNF
� Repeatedly apply resolution to clauses or copies of clauses until either
the empty clause (contradiction) is derived or no more clauses can be
derived (a copy of a clause is the clause with all variables renamed)
� If the empty clause is derived, answer ‘yes’ (query follows from
knowledge base), otherwise answer ‘no’ (query does not follow from
knowledge base) . . . and if there are an infinite number of clauses that
can be derived, don’t answer at all
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 20
First-Order Resolution
A1∨·· ·∨Am∨B ¬B
′∨C1∨·· ·∨Cn
(A1∨·· ·∨Am∨C1∨·· ·∨Cn)θ
❧
❧
❧
❧
❧
❧
❧❧
✱
✱
✱
✱
✱
✱
✱✱
where B, B′ are positive literals, Ai, C j are literals, θ is an mgu of B and B
′
� B and ¬B′ are complementary literals
� (A1∨·· ·∨Am∨C1∨·· ·∨Cn)θ is the resolvent of the two clauses
� Special case: If no Ai and C j, resolvent is empty clause, denoted �
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 23
Resolution: Example 2
⊢ ∃x∀y∀z((P(y)∨Q(z))→ (P(x)∨Q(x)))
1. P( f (x))∨Q(g(x)) [¬ Query]
2. ¬P(x) [¬ Query]
3. ¬Q(x) [¬ Query]
4. ¬P(y) [Copy of 2]
5. Q(g(x)) [1, 4 Resolution {y/ f (x)}]
6. ¬Q(z) [Copy of 3]
7. � [5, 6 Resolution {z/g(x)}]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 22
Resolution: Example 1
⊢ ∃x(P(x)→∀xP(x))
CNF(¬∃x(P(x)→∀xP(x)))
1, 2. ∀x¬(¬P(x)∨∀xP(x))
2. ∀x(¬¬P(x)∧¬∀xP(x))
2, 3. ∀x(P(x)∧∃x¬P(x))
4. ∀x(P(x)∧∃y ¬P(y))
5. ∀x∃y(P(x)∧¬P(y))
6. ∀x(P(x)∧¬P( f (x)))
8. P(x), ¬P( f (x))
1. P(x) [¬ Query]
2. ¬P( f (y)) [Copy of ¬ Query]
3. � [1, 2 Resolution {x/ f (y)}]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 25
Examples
� S = { f (x,g(x)), f (h(y),g(h(z)))}
D0 = {x,h(y)} so σ1 = {x/h(y)}
S1 = { f (h(y),g(h(y))), f (h(y),g(h(z)))}
D1 = {y,z} so σ2 = {x/h(z),y/z}
S2 = { f (h(z),g(h(z))), f (h(z),g(h(z)))}
i.e. σ2 is an mgu
� S = { f (h(x),g(x)), f (g(x),h(x))} . . .?
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 24
Unification Algorithm
� The disagreement set of S: Find the leftmost position at which not all
members E of S have the same symbol; the set of subexpressions of
each E in S that begin at this position is the disagreement set of S.
� Algorithm
1. S0 = S, σ0 = {}, i = 0
2. If Si is not a singleton find its disagreement set Di, otherwise
terminate with σi as the most general unifier
3. If Di contains a variable vi and term ti such that vi does not occur
in ti then
σi+1 = σi{vi/ti}, Si+1 = Si{vi/ti}
otherwise terminate as S is not unifiable
4. i = i+1; resume from step 2
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 27
Logic and Prolog
� Prolog stands for programming in logic
� Prolog is based on resolution refutation in first-order logic, but with
additional imposed search control rules
� How does the implementation of Prolog relate to logic?
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 26
Soundness and Completeness
For First-Order Logic
� Resolution refutation is sound, i.e. it preserves truth (if a set of
premises are all true, any conclusion drawn from those premises must
also be true)
� Resolution refutation is complete, i.e. it is capable of proving all
consequences of any knowledge base (not shown here!)
� Resolution refutation is not decidable, i.e. there is no algorithm
implementing resolution which when asked whether S ⊢ P, can
always answer ‘yes’ or ‘no’ (correctly)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 29
Undecidability of First-Order Logic
� Can we determine in general when this problem will arise? No!
� There is no general procedure
if (KB unsatisfiable)
return yes
else return no
� Resolution refutation is complete so if KB is unsatisfiable, the search
tree will contain the empty clause somewhere
� . . . but if the search tree does not contain the empty clause the search
may go on forever
� Even in the propositional case (which is decidable), complexity of
resolution is O(2n) for problems of size n
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 28
Undecidability of First-Order Logic
� KB = {P( f (x))→ P(x)}
� Q = P(a)?
� Obviously KB 6|= Q
� However, now try to show this using resolution
~P(f(x)) v P(x) ~P(a)
~P(f(a))
~P(f(f(a))
~P(f(f(f(a)))
…
x/a
x/f(a)
x/f(f(a))
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 31
SLD Resolution – ⊢SLD
� Selected literals Linear form Definite clauses resolution
� SLD refutation of a clause C from a set of clauses KB is a sequence
1. First clause of sequence is C
2. Each intermediate clause Ci is derived by resolving the previous
clause Ci−1 and a copy of a clause from KB
3. The last clause in the sequence is �
C1
…
C2
C
KB
� Theorem. For a definite KB and negative clause query Q: KB∪Q ⊢�
if and only if KB∪Q ⊢SLD �
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 30
Horn Clauses
Idea: Use less expressive language
� Review
◮ literal – atomic formula or negation of atomic formula
◮ clause – disjunction of literals
� Definite Clause – exactly one positive literal
◮ e.g. B∨¬A1∨ . . .∨¬An, i.e. B← A1∧ . . .∧An
� Negative Clause – no positive literals
◮ e.g. ¬Q1∨¬Q2 (negation of a query)
� Horn Clause – clause with at most one positive literal
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 33
Prolog Example
r(a,b). # facts
u(a).
v(b).
q(X) :- r(X,b), u(X). # rules
s(f(X)) :- v(X).
p(X) :- q(X), r(X,Z), s(f(Z)).
?- p(X). # query
X = a
Can give answer substitutions
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 32
Prolog
� Horn clauses in First-Order Logic
� SLD resolution
� Depth-first search strategy with backtracking
� User control
◮ Ordering of clauses in Prolog database (facts and rules)
◮ Ordering of subgoals in body of a rule
� Prolog is a programming language based on resolution refutation
relying on the programmer to exploit search control rules
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 35
Negation as Failure
� Prolog does not implement classical negation
◮ KB ⊢ ¬G if KB can prove ¬G
� Prolog not is known as negation as failure
◮ KB ⊢ not(G) if all attempts to prove G from KB fail
� Negation as failure is finite failure
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 34
Prolog Interpreter
Input: A query Q and a logic program KB
Output: ‘yes’ if Q follows from KB, ‘no’ otherwise
Initialize current goal set to {Q}
while the current goal set is not empty do
Choose G from the current goal set (first in goal set)
Choose a copy G′ :- B1, . . . ,Bn of a rule from KB for which
most general unifier of G,G′ is θ (try all in KB)
(if no such rule, undo unifications and try alternative rules)
Apply θ to the current goal set
Replace Gθ by B1θ, . . . ,Bnθ in current goal set
if current goal set is empty
output yes
else output no
� Depth-first, left-right with backtracking
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 37
Conclusion
� First-order logic can express objects, properties of objects and
relationships between objects, and allows quantification over
variables
� First-order logic is highly expressive
� Resolution refutation is sound and complete, but not decidable
� Prolog is more programming language than theorem prover
� Gödel’s incompleteness theorem
◮ Any first-order logic system with Peano’s axioms for arithmetic
cannot be both consistent and prove all true statements (where
statements are encoded using numbers)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 First-Order Logic 36
Soundness and Completeness Again
� Prolog including negation as failure is not sound, i.e. it does not
preserve truth
� Pure Prolog (without negation as failure) is not complete, i.e. it is
incapable of proving all consequences of any knowledge base (this is
because of the search order)
� Even pure Prolog is not decidable, i.e. the Prolog implementation of
resolution when asked whether KB ⊢ Q, can not always answer ‘yes’
or ‘no’ (correctly)
UNSW ©W. Wobcke et al. 2019–2021