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 (t0, . . . , tn) ▸ Relations R(t0, . . . , tn) and equality t0 = t1 ▸ Operators ∧, ∨, ¬, →, ↔ ▸ Quantifiers ∃xφ, ∀xφ Semantics A ⊧ φ(¯a) A = ⟨A, R0, R1, . . . , f0, f1, . . . ⟩ Examples φ = ∀x∃y[f (y) = x] , ψ = ∀x∀y∀z[x ≤ y ∧ y ≤ z → x ≤ z] . Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form Eliminate existential quantifiers: replace ∀¯x∃yφ(¯x, y) by ∀¯xφ(¯x, f (¯x)) ( f new symbol). Example ∀x∃y∃z[y > x ∧ z < x] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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 + 1 ≠ x] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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 + 1 ≠ x] ∀y[y + 1 ≠ c] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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 + 1 ≠ x] ∀y[y + 1 ≠ c] ∃x∀y∃z∀u∃v[R(x, y, z, u, v)] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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 + 1 ≠ x] ∀y[y + 1 ≠ c] ∃x∀y∃z∀u∃v[R(x, y, z, u, v)] ∀y∀u[R(c, y, f (y), u, g(y, z))] Normal Forms Prenex normal form Q0x0⋯Qnxnψ(¯x) , ψ quantifier-free Skolem normal form 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 + 1 ≠ x] ∀y[y + 1 ≠ 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 ¯t0, . . . ,¯tn such that the disjunction ⋁i≤n φ(¯ti) is valid. Corollary A formula ∀¯xφ(¯x) is unsatisfiable if, and only if, there are terms ¯t0, . . . ,¯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, x) x ↦ c x ↦ g(c) s = f (x, g(x)) t = f (x, y) x ↦ x x ↦ x y ↦ g(x) x ↦ 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), R0(¯t0), . . . , Rm(¯tm)} C′ = {¬P(¯s′ ), S0(¯u0), . . . , 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 {R0(σ(¯t0)), . . . , Rm(σ(¯tm)), S0(τ(¯u0)), . . . , 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, Σ, ∆, q0, F+, F−⟩ Q set of states Σ tape alphabet ∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−1, 0, 1} × Q q0 initial state F+ accepting states F− rejecting states Proof Turing machine M = ⟨Q, Σ, ∆, q0, F+, F−⟩ Q set of states Σ tape alphabet ∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−1, 0, 1} × Q q0 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 + 1 φ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 + 1 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 + 1 Initialisation formula for input: a0 . . . an−1 INIT = Sq0 (0) initial state ∧ h(0) = 0 initial head position ∧ ⋀ k