IA: Computational Logic
. Propositional Logic
Achim Blumensath blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Basic Concepts
Propositional Logic
Syntax
▸ Variables A, B, C, . . . , X, Y, Z, . . .
▸ Operators ∧, ∨, ¬, →, ↔
Examples
φ ∶= A ∧ (A → B) → B ,
ψ ∶= ¬(A ∧ B) ↔ (¬A ∨ ¬B) .
Terminology
▸ entailment φ ⊧ ψ
▸ equivalence φ ≡ ψ
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
Terminology
▸ entailment φ ⊧ ψ
▸ equivalence φ ≡ ψ
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is
Terminology
▸ entailment φ ⊧ ψ
▸ equivalence φ ≡ ψ
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is
Terminology
▸ entailment φ ⊧ ψ
▸ equivalence φ ≡ ψ
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is satisfiable but not valid.
▸ ¬A ∧ A is
Terminology
▸ entailment φ ⊧ ψ
▸ equivalence φ ≡ ψ
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is satisfiable but not valid.
▸ ¬A ∧ A is not satisfiable.
Normal Forms
Conjunctive Normal Form (CNF)
(A ∨ ¬B) ∧ (¬A ∨ C) ∧ (A ∨ ¬B ∨ ¬C)
Disjunctive Normal Form (DNF)
(A ∧ C) ∨ (¬A ∧ ¬B) ∨ (A ∧ ¬B ∧ ¬C)
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Example
CNF φ ∶= (A ∨ ¬B ∨ C) ∧ (¬A ∨ C) ∧ B
clauses {A, ¬B, C}, {¬A, C}, {B}
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Example
CNF φ ∶= (A ∨ ¬B ∨ C) ∧ (¬A ∨ C) ∧ B
clauses {A, ¬B, C}, {¬A, C}, {B}
Notation
Φ[L ∶= true] ∶= {C ∖ {¬L} C ∈ Φ , L ∉ C } .
The Satisfiability Problem
Davis-Putnam-Logemann-Loveland (DPLL) Algorithm
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
DPLL(Φ)
for every singleton {L} in Φ (* simplify Φ *)
Φ ∶= Φ[L ∶= true]
for every literal L whose negation does not occur in Φ
Φ ∶= Φ[L ∶= true]
if Φ contains the empty clause then (* are we done? *)
return false
if Φ is empty then
return true
choose some literal L in Φ (* try L ∶= true and L ∶= false *)
if DPLL(Φ[L ∶= true]) then
return true
else
return DPLL(Φ[L ∶= false])
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step : B ∶= true
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step : B ∶= true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step : C ∶= false and D ∶= false
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step : B ∶= true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step : C ∶= false and D ∶= false
{D}, {¬D}
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step : B ∶= true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step : C ∶= false and D ∶= false
{D}, {¬D}
∅ failure
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step : B ∶= false
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step : B ∶= false
{C, D}, {¬C, ¬D}
Step : C ∶= true
Example
Φ ∶= {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step : A ∶= true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step : B ∶= false
{C, D}, {¬C, ¬D}
Step : C ∶= true
{¬D} satisfiable
Solution: A = true, B = false, C = true, D = false
The Satisfiability Problem
Theorem
-SAT (satisfiability for formulae in -CNF) is NP-complete.
Proof
Turing machine M = ⟨Q, Σ, ∆, q, F+, F−⟩
Q set of states
Σ tape alphabet
∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−, , } × Q
q initial state
F+ accepting states
F− rejecting states
nondeterministic, runtime bounded by the polynomial r(n)
Proof
Turing machine M = ⟨Q, Σ, ∆, q, F+, F−⟩
Q set of states
Σ tape alphabet
∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−, , } × Q
q initial state
F+ accepting states
F− rejecting states
nondeterministic, runtime bounded by the polynomial r(n)
Encoding in PL
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
φw ∶= ⋀
t<r(n)
[ADMt ∧ INIT ∧ TRANSt ∧ ACC]
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Admissibility formula
ADMt ∶= ⋀
p≠q
[¬St,p ∨ ¬St,q] unique state
∧ ⋀
k≠l
[¬Ht,k ∨ ¬Ht,l] unique head position
∧ ⋀
k
⋀
a≠b
[¬Wt,k,a ∨ ¬Wt,k,b] unique letter
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Initialisation formula for input: a . . . an−
INIT ∶= S,q initial state
∧ H, initial head position
∧ ⋀
k<n
W,k,ak
∧ ⋀
n≤k≤r(n)
W,k,◻ initial tape content
Acceptance formula
ACC ∶= ⋁
q∈F+
⋁
t≤r(n)
St,q accepting state
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Transition formula
TRANSt ∶= ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+,q ∧ Ht+,k−m ∧ Wt+,k,b]
effect of transition
∧ ⋀
k≤r(n)
⋀
a∈Σ
[¬Ht,k ∧ Wt,k,a → Wt+,k,a]
rest of tape remains unchanged
Proof
TRANSt ∶= ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+,q ∧ Ht+,k+m ∧ Wt+,k,b] ∧ . . .
Proof
TRANSt ∶= ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+,q ∧ Ht+,k+m ∧ Wt+,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+,q]
TS(p, a) ∶= {q ∈ Q ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
TRANSt ∶= ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+,q ∧ Ht+,k+m ∧ Wt+,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+,q]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+,q → ⋁
m∈TH(p,a,q)
Ht+,k+m]
TH(p, a, q) ∶= {m ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
TRANSt ∶= ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+,q ∧ Ht+,k+m ∧ Wt+,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+,q]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+,q → ⋁
m∈TH(p,a,q)
Ht+,k+m]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
⋀
m∈{−,,}
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+,q ∧ Ht+,k+m →
⋁
b∈TW(p,a,m,q)
Wt+,k,b]
TW(p, a, m, q) ∶= {b ∈ Q ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
Properties of φw
▸ It is in CNF.
▸ It has length ∼ r(n)
.
▸ It is satisfiable if, and only if, the Turing machine accepts w.
Consequently, the satisfiability problem for PL-formulae in CNF is
NP-complete.
Proof
Properties of φw
▸ It is in CNF.
▸ It has length ∼ r(n)
.
▸ It is satisfiable if, and only if, the Turing machine accepts w.
Consequently, the satisfiability problem for PL-formulae in CNF is
NP-complete.
Reduction to -CNF
{L, L, L, . . . , Ln} ↦ {L, L, X}, {¬X, L, . . . , Ln}
(X new variable)
Resolution
Resolution
Resolution Step
The resolvent of two clauses
C = {L, A, . . . , Am} and C′
= {¬L, B, . . . , Bn}
is the clause
{A, . . . , Am, B, . . . , Bn} .
Lemma
Let C be the resolvent of two clauses in Φ. Then
Φ ⊧ Φ ∪ {C} .
The Resolution Method
Observation
If Φ contains the empty clause ∅, then Φ is not satisfiable.
Resolution Method
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
RM(Φ)
add to Φ all possible resolvents
repeat until no new clauses are generated
if ∅ ∈ Φ then
return false
else
return true
Theorem
The resolution method for propositional logic is sound and complete.
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
{A, B} {¬A, B} {¬B, ¬C}
{B} {¬B}
∅
Davis-Putnam Algorithm
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
DP(Φ)
remove all tautological clauses from Φ
if Φ = ∅ then
return true
if Φ = {∅} then
return false
select a variable X
add to Φ all resolvents over X
remove all clauses containing X or ¬X from Φ
repeat
Horn formulae
Linear Resolution
A linear resolution is a sequence of resolution steps where in each step
the resolvent of the previous step is used.
{¬A, ¬B} {A, ¬C} {B, ¬C, ¬D} {C, ¬D} {D}
{¬B, ¬C}
{¬C, ¬D}
{¬D}
∅
Horn formulae and linear resolution
Horn formulae
A Horn clause is a clause C that contains at most one positive literal.
Example
A ∧ ⋅⋅⋅ ∧ An → B ≡ {¬A, . . . , ¬An, B}
Horn formulae and linear resolution
Horn formulae
A Horn clause is a clause C that contains at most one positive literal.
Example
A ∧ ⋅⋅⋅ ∧ An → B ≡ {¬A, . . . , ¬An, B}
Theorem
A set of Horn clauses is unsatisfiable if, and only if, one can use linear
resolution to derive the empty clause from it.
SLD Resolution
Linear resolution where the clauses are sequences instead of sets and
we always resolve the leftmost literal of the current clause.
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Algorithm to compute it:
Input: Φ set of Horn-formulae
T ∶= ∅
repeat
for all A ∧ ⋅⋅⋅ ∧ An− → B ∈ Φ do
if A, . . . , An− ∈ T then
T ∶= T ∪ {B}
until T does not change anymore
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Algorithm to compute it:
Input: Φ set of Horn-formulae
T ∶= ∅
repeat
for all A ∧ ⋅⋅⋅ ∧ An− → B ∈ Φ do
if A, . . . , An− ∈ T then
T ∶= T ∪ {B}
until T does not change anymore
Theorem
Satisfiability for sets of Horn-formulae can be checked in linear time.
Finite Games G = ⟨V , V◻, E⟩
Players and ◻
◻
◻
◻
◻
◻
◻
Winning regions: W , W◻
Finite Games G = ⟨V , V◻, E⟩
Players and ◻
◻
◻
◻
◻
◻
◻
Winning regions: W , W◻
Reduction
positions
V = variables ⟨A⟩ and V◻ = formulae [A ∧ ⋅⋅⋅ ∧ An− → B]
edges
⟨B⟩ → [A ∧ ⋅⋅⋅ ∧ An− → B]
[A ∧ ⋅⋅⋅ ∧ An− → B] → ⟨Ai⟩
Lemma
A variable A belongs to W iff it is true in the minimal model.
B ∧ C → A A ∧ D → B F → C
D ∧ E → A C ∧ F → B  → F
⟨F⟩
[F → C]
[C ∧ F → B]
⟨C⟩
⟨B⟩
[B ∧ C → A]
[A ∧ D → B]
⟨A⟩
⟨D⟩
[D ∧ E → A] ⟨E⟩
[ → F]
Simple Algorithm
Win(v, σ)
if v ∈ Vσ then
if there is an edge v → u with Win(u, σ) then
return true
else
return false
if v ∈ Vσ then (* ∶= ◻ ◻ ∶= *)
if for every edge v → u we have Win(u, σ) then
return true
else
return false
Linear Algorithm
Input: game ⟨V , V◻, E⟩
forall v ∈ V do
win[v] ∶= (* winner of the position *)
P[v] ∶= ∅ (* set of predecessors of v *)
n[v] ∶=  (* number of successors of v *)
end
forall ⟨u, v⟩ ∈ E do
P[v] ∶= P[v] ∪ {u}
n[u] ∶= n[u] + 
end
forall v ∈ V do
if n[v] =  then Propagate(v, ◻)
forall v ∈ V◻ do
if n[v] =  then Propagate(v, )
return win
procedure Propagate(v, σ) =
if win[v] ≠ then return
win[v] ∶= σ
forall u ∈ P[v] do
n[u] ∶= n[u] − 
if u ∈ Vσ or n[u] =  then Propagate(u, σ)
end
end