IA008: Computational Logic
4. Deduction
Achim Blumensath blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Tableaux
Tableau Proofs
For simplicity: first-order logic without equality
Statements φ true or φ false
Rule
φ σ
ψ0 τ0
. . .
θ0 υ0
ψm τm
θm υm
Interpretation
If φ σ is possible then so is ψi τi,...,θi υi, for some i.
Tableaux
Construction
A tableau for a formula φ is constructed as follows:
▸ start with φ false
▸ choose a branch of the tree
▸ choose a statement ψ value on the branch
▸ choose a rule with head ψ value
▸ add it at the bottom of the branch
▸ repeat until every branch contains both statements ψ true and
ψ false for some formula ψ
¬φ true
φ false
¬φ false
φ true
φ ∧ ψ true
φ true
ψ true
φ ∧ ψ false
φ false ψ false
φ ∨ ψ true
φ true ψ true
φ ∨ ψ false
φ false
ψ false
φ → ψ true
φ false ψ true
φ → ψ false
φ true
ψ false
φ ↔ ψ true
φ true
ψ true
φ false
ψ false
φ ↔ ψ false
φ true
ψ false
φ false
ψ true
∀xφ true
φ[x ↦ t] true
∀xφ false
φ[x ↦ c] false
∃xφ true
φ[x ↦ c] true
∃xφ false
φ[x ↦ t] false
c a new constant symbol, t an arbitrary term
Example
(A ∨ B) → ¬(¬A ∧ ¬B) false ¬(¬A ∧ ¬B) → (A ∨ B) false
Example
(A ∨ B) → ¬(¬A ∧ ¬B) false
A ∨ B true
¬(¬A ∧ ¬B) false
¬A ∧ ¬B true
¬A true
¬B true
A false
B false
A true B true
¬(¬A ∧ ¬B) → (A ∨ B) false
¬(¬A ∧ ¬B) true
A ∨ B false
A false
B false
¬A ∧ ¬B false
¬A false ¬B false
A true B true
Example
∃x∀yR(x, y) → ∀y∃xR(x, y) false ∀xR(x, x) → ∀x∃yR(f(x), y) false
Example
∃x∀yR(x, y) → ∀y∃xR(x, y) false
∃x∀yR(x, y) true
∀y∃xR(x, y) false
∀yR(c, y) true
∃xR(x, d) false
R(c, d) true
R(c, d) false
∀xR(x, x) → ∀x∃yR(f(x), y) false
∀xR(x, x) true
∀x∃yR(f(x), y) false
∃yR(f(c), y) false
R(f(c), f(c)) false
R(f(c), f(c)) true
Soundness and Completeness
吀heorem
A first-order formula φ is valid if, and only if, there exists a tableau T
for φ false where every branch is contradictory.
Soundness and Completeness
吀heorem
A first-order formula φ is valid if, and only if, there exists a tableau T
for φ false where every branch is contradictory.
Corollary
Validity of first-order formulae is recursively enumerable, but not
decidable.
Soundness and Completeness
吀heorem
A first-order formula φ is valid if, and only if, there exists a tableau T
for φ false where every branch is contradictory.
Terminology
A tableau for a statement φ value is a tableau T where the root is
labelled with φ value.
A branch β is contradictory if it contains both statements ψ true
and ψ false, for some formula ψ.
A branch β is consistent with a structure A if
▸ A ⊧ ψ, for all statements ψ true on β and
▸ A ⊭ ψ, for all statements ψ false on β.
A branch β is complete if, for every atomic formula ψ, it contains
one of the statements ψ true or ψ false.
Proof Sketch: Soundness
Lemma
If β is consistent with A and we extend the tableau by applying a
rule, the new tableau has a branch β′
extending β that is consistent
with A.
Corollary
If A ⊭ φ, then every tableau for φ false has a branch that is not
contradictory.
Corollary
If φ is not valid, there is no tableau for φ false where all branches are
contradictory.
Proof Sketch: Completeness
Lemma
If every tableau for φ false has a non-contradictory branch, there
exists a tableau for φ false with a branch β that is complete and
non-contradictory.
Lemma
If a branch β is complete and non-contradictory, there exists a
structure A such that β is consistent with A.
Corollary
If every tableau for φ false has a non-contradictory branch, there
exists a structure A with A ⊭ φ.
Natural Deduction
Proof Calculi
Notation
ψ1,...,ψn ⊢ φ φ is provable with assumptions ψ1,...,ψn
Proof Calculi
Notation
ψ1,...,ψn ⊢ φ φ is provable with assumptions ψ1,...,ψn
φ is provable if ⊢ φ.
Proof Calculi
Notation
ψ1,...,ψn ⊢ φ φ is provable with assumptions ψ1,...,ψn
φ is provable if ⊢ φ.
Rules
Γ1 ⊢ φ1 ... Γn ⊢ φn
Δ ⊢ ψ
premises
conclusion
φ1 ∧ ⋅⋅⋅ ∧ φn ⇒ ψ
Proof Calculi
Notation
ψ1,...,ψn ⊢ φ φ is provable with assumptions ψ1,...,ψn
φ is provable if ⊢ φ.
Rules
Γ1 ⊢ φ1 ... Γn ⊢ φn
Δ ⊢ ψ
premises
conclusion
φ1 ∧ ⋅⋅⋅ ∧ φn ⇒ ψ
Axiom
Δ ⊢ ψ
rule without premises
Proof Calculi
Notation
ψ1,...,ψn ⊢ φ φ is provable with assumptions ψ1,...,ψn
φ is provable if ⊢ φ.
Rules
Γ1 ⊢ φ1 ... Γn ⊢ φn
Δ ⊢ ψ
premises
conclusion
φ1 ∧ ⋅⋅⋅ ∧ φn ⇒ ψ
Axiom
Δ ⊢ ψ
rule without premises
Remark
Tableaux speak about possibilities while Natural Deduction proofs
speak about necesseties.
Proof Calculi
Derivation
Γ ⊢ φ Δ0 ⊢ ψ0
Δ1 ⊢ ψ1 Γ′ ⊢ φ′
Σ ⊢ θ
tree of rules
Natural Deduction (propositional part)
(I⊺)
Γ ⊢ ⊺
(Ax)
Γ,φ ⊢ φ
(I∧)
Γ ⊢ φ Δ ⊢ ψ
Γ,Δ ⊢ φ ∧ ψ
(E∧)
Γ ⊢ φ ∧ ψ
Γ ⊢ φ
Γ ⊢ φ ∧ ψ
Γ ⊢ ψ
(I∨)
Γ,¬ψ ⊢ φ
Γ ⊢ φ ∨ ψ
Γ,¬φ ⊢ ψ
Γ ⊢ φ ∨ ψ
(E∨)
Γ ⊢ φ ∨ ψ Δ,φ ⊢ θ Δ′
,ψ ⊢ θ
Γ,Δ,Δ′ ⊢ θ
(I¬)
Γ,φ ⊢
Γ ⊢ ¬φ
(E¬)
Γ,¬φ ⊢
Γ ⊢ φ
(I )
Γ ⊢ φ Γ ⊢ ¬φ
Γ ⊢
(E )
Γ ⊢
Γ ⊢ φ
(I→)
Γ,φ ⊢ ψ
Γ ⊢ φ → ψ
(E→)
Γ ⊢ φ Δ ⊢ φ → ψ
Γ,Δ ⊢ ψ
(I↔)
Γ,φ ⊢ ψ Δ,ψ ⊢ φ
Γ,Δ ⊢ φ ↔ ψ
(E↔)
Γ ⊢ φ Δ ⊢ φ ↔ ψ
Γ,Δ ⊢ ψ
( + sym.)
Examples
⊢ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ)
Examples
φ ∨ ψ,¬φ ∧ ¬ψ ⊢ φ ∨ ψ
φ ⊢ φ
¬φ ∧ ¬ψ ⊢ ¬φ ∧ ¬ψ
¬φ ∧ ¬ψ ⊢ ¬φ
φ,¬φ ∧ ¬ψ ⊢
⋯
ψ,¬φ ∧ ¬ψ ⊢
φ ∨ ψ,¬φ ∧ ¬ψ ⊢
φ ∨ ψ ⊢ ¬(¬φ ∧ ¬ψ)
⊢ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ)
Natural Deduction (quantifiers and equality)
(I∃)
Γ ⊢ φ[x ↦ t]
Γ ⊢ ∃xφ
(E∃)
Γ ⊢ ∃xφ Δ,φ[x ↦ c] ⊢ ψ
Γ,Δ ⊢ ψ
(I∀)
Γ ⊢ φ[x ↦ c]
Γ ⊢ ∀xφ
(E∀)
Γ ⊢ ∀xφ
Γ ⊢ φ[x ↦ t]
(I=)
Γ ⊢ t = t
(E=)
Γ ⊢ s = t Δ ⊢ φ[x ↦ s]
Γ,Δ ⊢ φ[x ↦ t]
c a new constant symbol, s,t arbitrary terms
Examples
s = t ⊢ t = s
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
s = t, t = u ⊢ s = u
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
s = t, t = u ⊢ s = u t = u ⊢ t = u s = t ⊢ s = t
s = t, t = u ⊢ s = u
(E=)
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
s = t, t = u ⊢ s = u t = u ⊢ t = u s = t ⊢ s = t
s = t, t = u ⊢ s = u
(E=)
∃x∀yR(x,y) ⊢ ∀y∃xR(x,y)
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
s = t, t = u ⊢ s = u t = u ⊢ t = u s = t ⊢ s = t
s = t, t = u ⊢ s = u
(E=)
∃x∀yR(x,y) ⊢ ∀y∃xR(x,y)
∃x∀yR(x,y) ⊢ ∃x∀yR(x,y)
∀yR(c,y) ⊢ ∀yR(c,y)
∀yR(c,y) ⊢ R(c,d)
(E∀)
∀yR(c,y) ⊢ ∃xR(x,d)
(I∃)
∀yR(c,y) ⊢ ∀y∃xR(x,y)
(I∀)
∃x∀yR(x,y) ⊢ ∀y∃xR(x,y)
(E∃)
Soundness and Completeness
吀heorem
A formula φ is provable using Natural Deduction if, and only if, it is
valid.
Corollary
吀he set of valid first-order formulae is recursively enumerable.
Isabelle/HOL
Isabelle/HOL
Proof assistant designed for so昀tware verification.
General structure
theory T
imports T1 ... Tn
begin
declarations, definitions, and proofs
end
Syntax
Two levels:
▸ the meta-language (Isabelle) used to define theories,
▸ the logical language (HOL) used to write formulae.
To distinguish the levels, one encloses formulae of the logical
language in quotes.
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
primrec app :: "'a list => '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.
⇒ 吀here 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
吀he system
α
α β
β
has a unique consistent set {α,β}.
吀he system
α
α β
γ
α γ
β
has consistent sets
{α,β}, {α,γ}, {α,β,γ} .