IA: Computational Logic . First-Order Logic Achim Blumensath blumens@fi.muni.cz Faculty of Informatics, Masaryk University, Brno Basic Concepts First-Order Logic Syntax ▸ Variables x, y, z, . . . ▸ Terms x, f (t, . . . , tn) ▸ Relations R(t, . . . , tn) and equality t = t ▸ Operators ∧, ∨, ¬, →, ↔ ▸ Quantifiers ∃xφ, ∀xφ Examples φ ∶= ∀x∃y[f (y) = x] , ψ ∶= ∀x∀y∀z[x ≤ y ∧ y ≤ z → x ≤ z] . Prenex Normal Form Qx⋯Qnxnψ(¯x) , ψ quantifier-free Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] ∃x∀y[y +  ≠ x] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] ∃x∀y[y +  ≠ x] ∀y[y +  ≠ c] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] ∃x∀y[y +  ≠ x] ∀y[y +  ≠ c] ∃x∀y∃z∀u∃v[R(x, y, z, u, v)] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] ∃x∀y[y +  ≠ x] ∀y[y +  ≠ c] ∃x∀y∃z∀u∃v[R(x, y, z, u, v)] ∀y∀u[R(c, y, f (y), u, g(y, z))] Skolemisation Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] ∀x[f (x) > x ∧ g(x) < x] ∃x∀y[y +  ≠ x] ∀y[y +  ≠ c] ∃x∀y∃z∀u∃v[R(x, y, z, u, v)] ∀y∀u[R(c, y, f (y), u, g(y, z))] Theorem Let φs be a Skolemisation of φ. Then φs is satisfiable iff φ is satisfiable. Theorem of Herbrand Theorem of Herbrand A formula ∃¯xφ(¯x) is valid if, and only if, there are terms ¯t, . . . ,¯tn such that the disjunction ⋁i≤n φ(¯ti) is valid. Corollary A formula ∀¯xφ(¯x) is unsatisfiable if, and only if, there are terms ¯t, . . . ,¯tn such that the conjunction ⋀i≤n φ(¯ti) is unsatisfiable. Substitution Definition A substitution σ is a function that replaces in a formula every free variable by a term (and renames bound variables if necessary). Instead of σ(φ) we also write φ[x ↦ s, y ↦ t] if σ(x) = s and σ(y) = t. Examples (x = f (y))[x ↦ g(x), y ↦ c] = g(x) = f (c) ∃z(x = z + z)[x ↦ z] = ∃u(z = u + u) Unification Definition A unifier of two terms s(¯x) and t(¯x) is a pair of substitution σ, τ such that σ(s) = τ(t). A unifier σ, τ is most general if every other unifier σ′ , τ′ can be written as σ′ = ρ ○ σ and τ′ = υ ○ τ, for some ρ, υ. Examples s = f (x, g(x)) t = f (c, y) x ↦ c, y ↦ g(c) s = f (x, g(x)) t = f (x, y) x ↦ x, y ↦ g(x) x ↦ g(x), y ↦ g(g(x)) s = f (x) t = g(x) unification not possible Unification Algorithm unify(s, t) if s is a variable x then set x to t else if t is a variable x then set x to s else s = f (¯u) and t = g(¯v) if f = g then forall i unify(ui, vi) else fail Union-Find-Algorithm   values ⎫⎪⎪⎪⎪⎪⎪⎪⎪ ⎬ ⎪⎪⎪⎪⎪⎪⎪⎪⎭ variables find ∶ variable → value ▸ follows pointers to the root and creates shortcuts union ∶ (variable × variable) → unit ▸ links roots by a pointer Resolution Clauses Definitions ▸ literal R(¯t) or ¬R(¯t) ▸ clause set of literals {P(¯s), R(¯t), ¬S(¯u)} Clauses Definitions ▸ literal R(¯t) or ¬R(¯t) ▸ clause set of literals {P(¯s), R(¯t), ¬S(¯u)} Example CNF φ ∶= ∀x∀y[R(x, y) ∨ ¬R(x, f (x))] ∧ ∀y[¬R(f (y), y) ∨ P(y)] (no existential quantifiers) clauses {R(x, y)¬R(x, f (x))}, {¬R(f (y), y), P(y)} Resolution Resolution Step Consider two clauses C = {P(¯s), R(¯t), . . . , Rm(¯tm)} C′ = {¬P(¯s′ ), S(¯u), . . . , Sn(¯un)} where ¯s and ¯s′ have no common variables, and let σ be the most general unifier of ¯s and ¯s′ . The resolvent of C and C′ is the clause {R(σ(¯t)), . . . , Rm(σ(¯tm)), S(σ(¯u)), . . . , Sn(σ(¯un))} . Lemma Let C be the resolvent of two clauses in Φ. Then Φ ⊧ Φ ∪ {C} . Example φ = ∀x∀y[P(x) ∧ x ≤ y → P(y)] ∧ ∀x[x ≤ f (x)] ∧ Pc ∧ ¬P(f (c)) {¬P(x), x ≰ y, P(y)} {x ≤ f (x)} {P(c)} {¬P(f (c))} {¬P(z), P(f (z))} {P(f (c))} ∅ x ↦ z y ↦ f (z) x ↦ z z ↦ c The Resolution Method Theorem The resolution method for first-order logic (without equality) is sound and complete. Theorem Satisfiability for first-order logic is undecidable. Proof Turing machine M = ⟨Q, Σ, ∆, a, F+, F−⟩ Q set of states Σ tape alphabet ∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−, , } × Q q initial state F+ accepting states F− rejecting states Proof Turing machine M = ⟨Q, Σ, ∆, a, F+, F−⟩ Q set of states Σ tape alphabet ∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−, , } × Q q initial state F+ accepting states F− rejecting states Encoding in FO Sq(t) state q at time t h(t) head in field h(t) at time t Wa(t, k) letter a in field k at time t s successor function s(n) = n +  φw ∶= ADM ∧ INIT ∧ TRANS ∧ ACC Proof Sq(t) state q at time t h(t) head in field h(t) at time t Wa(t, k) letter a in field k at time t s successor function s(n) = n +  Admissibility formula ADM ∶= ∀t ⋀ p≠q ¬[Sp(t) ∧ Sq(t)] unique state ∧ ∀t∀k ⋀ a≠b ¬[Wa(t, k) ∧ Wb(t, k)] unique letter Proof Sq(t) state q at time t h(t) head in field h(t) at time t Wa(t, k) letter a in field k at time t s successor function s(n) = n +  Initialisation formula for input: a . . . an− INIT ∶= Sq () initial state ∧ h() =  initial head position ∧ ⋀ k