IA008: Computational Logic 2. 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] . Examples Structures • graphs G = ⟨V,E⟩ E ⊆ V × V binary relation Examples Structures • graphs G = ⟨V,E⟩ E ⊆ V × V binary relation • words W = ⟨W,≤,(Pa)a⟩ ≤ ⊆ W × W linear ordering Pa ⊆ W positions with letter a Examples Structures • graphs G = ⟨V,E⟩ E ⊆ V × V binary relation • words W = ⟨W,≤,(Pa)a⟩ ≤ ⊆ W × W linear ordering Pa ⊆ W positions with letter a • transition systems S = ⟨S,(Ea)a,(Pi)i⟩ Ea ⊆ V × V binary relation Pi ⊆ V unary relation Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x,y) → E(y,x)] Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x,y) → E(y,x)] • ‘吀he graph has no isolated vertices.’ Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x,y) → E(y,x)] • ‘吀he graph has no isolated vertices.’ ∀x∃y[E(x,y) ∨ E(y,x)] Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x,y) → E(y,x)] • ‘吀he graph has no isolated vertices.’ ∀x∃y[E(x,y) ∨ E(y,x)] • ‘Every vertex has outdegree 1.’ Examples Graphs G = ⟨V,E⟩, E ⊆ V × V • ‘吀he graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x,y) → E(y,x)] • ‘吀he graph has no isolated vertices.’ ∀x∃y[E(x,y) ∨ E(y,x)] • ‘Every vertex has outdegree 1.’ ∀x∃y[E(x,y) ∧ ∀z[E(x,z) → z = y]] 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,u))] 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). 吀heorem Let φs be a Skolemisation of φ. 吀hen φs is satisfiable iff φ is satisfiable. 吀heorem of Herbrand 吀heorem 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. Resolution 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 substitutions σ,τ 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 if x already has some value u then unify(u,t) else set x to t else if t is a variable x then if x already has some value v then unify(s,v) else 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 3 7 values ⎫⎪⎪⎪⎪⎪⎪⎪ ⎬ ⎪⎪⎪⎪⎪⎪⎪⎭ variables find variable → value ▸ follows pointers to the root and creates shortcuts union (variable × variable) → unit ▸ links roots by a pointer 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′ . 吀he 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 Φ. 吀hen Φ ⊧ Φ ∪ {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))} 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 吀he Resolution Method 吀heorem 吀he resolution method for first-order logic (without equality) is sound and complete. 吀heorem Satisfiability for first-order logic is undecidable. Satisfiability 吀heorem Satisfiability for first-order logic is undecidable. Proof Turing machine M = ⟨Q,Σ,Δ,q0,F+,F−⟩, non-deterministic 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 By adding a counter to M we may assume that every run of M terminates. Proof Turing machine M = ⟨Q,Σ,Δ,q0,F+,F−⟩, non-deterministic 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 0 zero φ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 0 zero 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