IA: Computational Logic
. 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
φ σ
ψ τ
. . .
ϑ υ
ψ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 ψ
R(¯t) true R(¯t) false ¬φ 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 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
∃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
Theorem
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
φ ∨ ψ, ¬φ ∧ ¬ψ ⊢ φ ∨ ψ
φ ⊢ φ
¬φ ∧ ¬ψ ⊢ ¬φ ∧ ¬ψ
¬φ ∧ ¬ψ ⊢ ¬φ
φ, ¬φ ∧ ¬ψ ⊢
⋯
ψ, ¬φ ∧ ¬ψ ⊢
φ ∨ ψ, ¬φ ∧ ¬ψ ⊢
φ ∨ ψ ⊢ ¬(¬φ ∧ ¬ψ)
⊢ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ)
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
Theorem
A formula φ is provable using Natural Deduction if, and only if, it is
valid.
Corollary
The set of valid first-order formulae is recursively enumerable.
Isabelle/HOL
Isabelle/HOL
Proof assistant designed for software 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)
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)
. add 0 0 = 0
. ⋀m. add m 0 = m ==> add (Suc m) 0 = Suc m
Proofs
lemma add_02: "add m 0 = m"
apply (induction m)
. add 0 0 = 0
. ⋀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)
. rev (rev Nil) = Nil
. ⋀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)
. rev (rev Nil) = Nil
. ⋀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)
. rev (rev Nil) = Nil
. ⋀x1 xs. rev (rev xs) = xs ==>
rev (rev (Cons x1 xs)) = Cons x1 xs
apply(auto)
. ⋀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)
. ⋀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)
. ⋀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)
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
{α, β}, {α, γ}, {α, β, γ} .