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 • ‘The graph is undirected.’ (i.e., E is symmetric) Examples Graphs G = ⟨V, E⟩, E ⊆ V × V • ‘The graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x, y) → E(y, x)] Examples Graphs G = ⟨V, E⟩, E ⊆ V × V • ‘The graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x, y) → E(y, x)] • ‘The graph has no isolated vertices.’ Examples Graphs G = ⟨V, E⟩, E ⊆ V × V • ‘The graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x, y) → E(y, x)] • ‘The graph has no isolated vertices.’ ∀x∃y[E(x, y) ∨ E(y, x)] Examples Graphs G = ⟨V, E⟩, E ⊆ V × V • ‘The graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x, y) → E(y, x)] • ‘The 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 • ‘The graph is undirected.’ (i.e., E is symmetric) ∀x∀y[E(x, y) → E(y, x)] • ‘The 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]] Satisfiability 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 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 'a list => 'a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" Logical Language Types ▸ base types: bool, nat, int,… ▸ type constructors: α list, α set,… ▸ function types: α ⇒ β ▸ type variables: 'a, 'b,… Terms ▸ application: f x y, x + y,… ▸ abstraction: λx.t ▸ type annoation: t α ▸ if b then t else u ▸ let x = t in u ▸ case x of p0 ⇒ t0 | ⋯ | pn ⇒ tn Formulae ▸ terms of type bool ▸ boolean operations ¬, ∧, ∨, → ▸ quantifiers ∀x, ∃x ▸ predicates ==, <,… Basic Types datatype bool = True | False fun conj :: "bool => bool => bool" where "conj True True = True" | "conj _ _ = False" datatype nat = 0 | Suc nat fun add :: "nat => nat => nat" where "add 0 n = n" | "add (Suc m) n = Suc (add m n)" lemma add_02: "add m 0 = m" apply (induction m) apply (auto) done Proofs lemma add_02: "add m 0 = m" Proofs lemma add_02: "add m 0 = m" apply (induction m) Proofs lemma add_02: "add m 0 = m" apply (induction m) 1. add 0 0 = 0 2. ⋀m. add m 0 = m ==> add (Suc m) 0 = Suc m Proofs lemma add_02: "add m 0 = m" apply (induction m) 1. add 0 0 = 0 2. ⋀m. add m 0 = m ==> add (Suc m) 0 = Suc m apply (auto) datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) fun app :: "'a list => 'a list => 'a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" fun rev :: "'a list => 'a list" where "rev [] = []" | "rev (x # xs) = (rev xs) @ (x # [])" theorem rev_rev [simp]: "rev (rev xs) = xs" theorem rev_rev [simp]: "rev (rev xs) = xs" apply(induction xs) theorem rev_rev [simp]: "rev (rev xs) = xs" apply(induction xs) 1. rev (rev Nil) = Nil 2. ⋀x1 xs. rev (rev xs) = xs ==> rev (rev (Cons x1 xs)) = Cons x1 xs theorem rev_rev [simp]: "rev (rev xs) = xs" apply(induction xs) 1. rev (rev Nil) = Nil 2. ⋀x1 xs. rev (rev xs) = xs ==> rev (rev (Cons x1 xs)) = Cons x1 xs apply(auto) theorem rev_rev [simp]: "rev (rev xs) = xs" apply(induction xs) 1. rev (rev Nil) = Nil 2. ⋀x1 xs. rev (rev xs) = xs ==> rev (rev (Cons x1 xs)) = Cons x1 xs apply(auto) 1. ⋀x1 xs. rev (rev xs) = xs ==> rev (rev xs @ Cons x1 Nil) = Cons x1 xs lemma app_Nil2 [simp]: "xs @ Nil = xs" apply(induction xs) apply(auto) done lemma app_Nil2 [simp]: "xs @ Nil = xs" apply(induction xs) apply(auto) done lemma rev_app [simp]: "rev (xs @ ys) = rev ys @ rev xs" apply(induction xs) apply(auto) 1. ⋀x1 xs. rev (xs @ ys) = rev ys @ rev xs ==> (rev ys @ rev xs) @ Cons x1 Nil = rev ys @ (rev xs @ Cons x1 Nil) lemma app_Nil2 [simp]: "xs @ Nil = xs" apply(induction xs) apply(auto) done lemma rev_app [simp]: "rev (xs @ ys) = rev ys @ rev xs" apply(induction xs) apply(auto) 1. ⋀x1 xs. rev (xs @ ys) = rev ys @ rev xs ==> (rev ys @ rev xs) @ Cons x1 Nil = rev ys @ (rev xs @ Cons x1 Nil) lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" apply (induction xs) apply (auto) done lemma app_Nil2 [simp]: "xs @ [] = xs" apply(induction xs) apply(auto) done lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" apply(induction xs) apply(auto) done lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" apply(induction xs) apply(auto) done theorem rev_rev [simp]: "rev(rev xs) = xs" apply(induction xs) apply(auto) done end Nonmonotonic Logic Negation as Failure Goal Develop a proof calculus supporting Negation as Failure as used in Prolog. Monotonicity Ordinary deduction is monotone: if we add new assumption, all consequences we have already derived remain. More information does not invalidate already made deductions. Non-Monotonicity Negation as Failure is non-monotone: P implies ¬Q but P, Q does not imply ¬Q . Default Logic Rule α0 . . . αm β0 . . . βn γ αi assumptions βi restraints γ consequence Derive γ provided that we can derive α0, . . . , αm, but none of β0, . . . , βn. Example bird(x) penguin(x) ostrich(x) can_fly(x) Semantics Definition A set Φ of formulae is consistent with respect to a set of rules R if, for every rule α0 . . . αm β0 . . . βn γ ∈ R such that α0, . . . , αm ∈ Φ and β0, . . . , βn ∉ Φ, we have γ ∈ Φ. Note If there are no restraints βi, consistent sets are closed under intersection. ⇒ There is a unique smallest such set, that of all provable formulae. If there are restraints, this may not be the case. Formulae that belong to all consistent sets are called secured consequences. Examples The system α α β β has a unique consistent set {α, β}. The system α α β γ α γ β has consistent sets {α, β}, {α, γ}, {α, β, γ} .