COMP30026 Models of Computation – Symbolic Deduction
COMP30026 Models of Computation
Symbolic Deduction
Bach Le / Anna Kalenkova
Lecture Week 3 Part 1 (Zoom)
Semester 2, 2021
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 1 / 27
This Lecture is Being Recorded
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 2 / 27
Mechanising Deduction
We must not think that computation . . . has place only in
numbers.
— T. Hobbes (1655)
Calculus ratiocinator: G. W. Leibniz (1679).
Propositional logic:
G. Boole, A. De Morgan, E. Schröder (19th century).
Predicate logic: G. Frege (1879).
Universal computers:
C. Babbage (19th century), A. Turing (20th century).
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 3 / 27
Propositional Logic is Decidable
Generating a truth table is just a way of systematically exploring the
truth value of a formula, for each possible truth assignment, that is,
using brute force.
Formulas are assumed to be finite, so this way we can always decide
if a formula is satisfiable, and whether it is valid.
Unfortunately truth tables may grow exponentially in the size of
formulas.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 4 / 27
Faster Satisfiability/Validity Checking?
Are there faster decision procedures for propositional logic?
It depends on how we choose to write the formulas.
What if we don’t want to commit to any particular form?
Then satisfiability is NP-complete and validity is co-NP-complete.
These are terms from complexity theory. Historically the satisfiability
problem for propositional logic, SAT, has been seminal for this theory.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 5 / 27
SAT and Complexity Theory
A who’s who of important problems in scheduling, network flow and
routing, database management, number theory, automata, circuit
fault detection, code generation, . . . , have been shown to be
tractable if and only if SAT is.
Most computer scientists conclude from this that it is unlikely that
there are decision procedures for SAT (and hence for all those other
problems) that perform much better than brute force.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 6 / 27
Normal Forms for Propositional Logic
A literal is P or ¬P where P is a propositional letter.
A formula is in conjunctive normal form (CNF) if it is a conjunction
of disjunctions of literals (a conjunction of “clauses”).
(A ∨ ¬B) ∧ (B ∨ C ∨ D) ∧ A
It is in disjunctive normal form (DNF) if it is a disjunction of
conjunctions of literals.
(¬A ∧ ¬B) ∨ (¬B ∧ C ) ∨ (A ∧ ¬D)
Theorem: Every propositional formula can be expressed in CNF, as
well as in DNF.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 7 / 27
Converting a Formula to CNF or to DNF
1 Eliminate all occurrences of ⊕, using
A⊕ B ≡ (A ∨ B) ∧ (¬A ∨ ¬B).
2 Eliminate all occurrences of ⇔, using
A⇔ B ≡ (A⇒ B) ∧ (B ⇒ A).
3 Eliminate all occurrences of ⇒ using A⇒ B ≡ ¬A ∨ B .
4 Use De Morgan’s Laws to push ¬ inward over ∧ and ∨.
5 Eliminate double negations using ¬¬A ≡ A.
6 Use the distributive laws to get the required form.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 8 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
≡ (¬(¬P ∧ (¬¬Q ∨ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (3)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
≡ (¬(¬P ∧ (¬¬Q ∨ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (3)
≡ ((¬¬P ∨ (¬¬¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (4)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
≡ (¬(¬P ∧ (¬¬Q ∨ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (3)
≡ ((¬¬P ∨ (¬¬¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (4)
≡ ((P ∨ (¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (Q ∨ R))) (5)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
≡ (¬(¬P ∧ (¬¬Q ∨ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (3)
≡ ((¬¬P ∨ (¬¬¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (4)
≡ ((P ∨ (¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (Q ∨ R))) (5)
≡ (((P ∨ ¬Q) ∧ (P ∨ ¬R)) ∨ S)
∧ ((¬S ∨ ¬P) ∧ (¬S ∨ (Q ∨ R))) (6)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Example Conversion to CNF
(¬P ∧ (¬Q ⇒ R))⇔ S
≡ ((¬P ∧ (¬Q ⇒ R))⇒ S) ∧ (S ⇒ (¬P ∧ (¬Q ⇒ R))) (2)
≡ (¬(¬P ∧ (¬Q ⇒ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬Q ⇒ R))) (3)
≡ (¬(¬P ∧ (¬¬Q ∨ R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (3)
≡ ((¬¬P ∨ (¬¬¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (¬¬Q ∨ R))) (4)
≡ ((P ∨ (¬Q ∧ ¬R)) ∨ S) ∧ (¬S ∨ (¬P ∧ (Q ∨ R))) (5)
≡ (((P ∨ ¬Q) ∧ (P ∨ ¬R)) ∨ S)
∧ ((¬S ∨ ¬P) ∧ (¬S ∨ (Q ∨ R))) (6)
≡ (P ∨ ¬Q ∨ S) ∧ (P ∨ ¬R ∨ S)
∧ (¬S ∨ ¬P) ∧ (¬S ∨ Q ∨ R) (6)
The result is in conjunctive normal form.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 9 / 27
Reduced CNF
There is one more transformation that it is easy and natural to do:
simplifying clauses.
A CNF formula is in reduced CNF (RCNF) if, for each of its clauses,
no propositional letter occurs twice.
The transformation is the obvious one, for example:
(A ∨ ¬B ∨ ¬A) ∧ (¬C ∨ ¬B) ∧ (C ∨ ¬A ∨ C ∨ B)
becomes
(¬C ∨ ¬B) ∧ (C ∨ ¬A ∨ B)
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 10 / 27
Normal Form Does Not Mean Unique Form
The formula
(P ∧ Q ∧ R) ∨ (¬P ∧ ¬Q ∧ ¬R) ∨ (¬P ∧ R) ∨ (Q ∧ ¬R)
is in reduced DNF, and so is the equivalent
¬P ∨ Q
So two DNF formulas may have different sizes and variables, and yet
be equivalent.
Similarly for (R)CNF.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 11 / 27
Canonical Forms: Xor Normal Form
If a normal form leads to a unique representation for every Boolean
function, we call it canonical.
One canonical form (“xor normal form”) presents the function in a
sum-of-products form, using exclusive or and conjunction.
For example, the formula (A⇒ B) ∧ (B ⊕ C ) is written as
ABC ⊕ AC ⊕ B ⊕ C
This form is unique, up to reordering of conjuncts and summands.
Or, representing the summands as sets:
{{A,B ,C}, {A,C}, {B}, {C}}
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 12 / 27
Canonical Forms: ROBDDs
Binary decision diagrams (BDDs) give another canonical form.
Here (A⇒ B) ∧ (B ⊕ C ) is represented by the graph
A
B B
C C
t f
Read: If A then [follow solid arc] else [follow dashed arc].
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 13 / 27
Validity and Satisfiability with ROBDDs
This graph representation becomes canonical when we enforce
maximal sharing of subgraphs (and agree on an ordering of variables,
like A, B , C ).
The resulting graph is then an ROBDD—a reduced, ordered BDD.
These have been very popular and useful for hardware verification etc.
Clearly a propositional formula is valid iff its ROBDD is the
single-leaf graph t .
It is unsatisfiable iff its ROBDD is f .
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 14 / 27
CNF and Clausal Form
Knowledge bases are often presented in CNF, as a set (conjunction)
of clauses.
A clause is a set (disjunction) of literals.
Abstracting from the order of literals and clauses, we can think of a
formula in CNF as given in clausal form, for example, we may write
(P ∨ ¬Q ∨ S) ∧ (P ∨ ¬R ∨ S) ∧ (¬S ∨ ¬P) ∧ (¬S ∨ Q ∨ R)
as
{{P, S ,¬Q}, {P, S ,¬R}, {¬P,¬S}, {Q,R ,¬S}}
We shall often make no distinction between these.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 15 / 27
Empty Clauses
Clause {A,B} represents A ∨ B , and clause {A} represents A.
How shall we read the clause ∅?
The natural reading is that it is false, because f is neutral element for
∨—we could have written A ∨ B as f ∨ A ∨ B , and A as f ∨ A.
Hence we agree that the empty clause ∅ represents ⊥.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 16 / 27
Empty CNF Formulas
The formula {C1,C2}, with clauses C1 and C2, represents C1 ∧ C2.
The formula {C} represents C .
How shall we read the (CNF) formula ∅?
The natural reading is that it is true, because t is neutral element for
∧—we could have written C1 ∧ C2 as t ∧ C1 ∧ C2, and C as t ∧ C .
Hence we agree that the empty formula ∅ represents ⊤.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 17 / 27
Empty Clauses and Formulas
For clausal form representation (CNF) we then have:
The set ∅ of clauses is valid.
Any set {∅, . . .} of clauses is unsatisfiable.
Don’t be confused by this.
An empty set of clauses is valid, because it is trivial to satisfy all of
the set’s clauses—there is nothing to do.
But a (non-empty) set that contains an empty clause cannot be
satisfied, because nothing satisfies that empty clause.
In particular, note that {∅} 6= ∅.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 18 / 27
Resolution-Based Inference
Consider the two clauses ¬P ∨ A and P ∨ B
If P is true, they reduce to A and t.
If P is false, they reduce to t and B .
There are no other possible values for P, so: if (¬P ∨A) and (P ∨B)
are both true, then either A is true or B is true (or both). That is,
the clause A ∨ B is a logical consequence of the two original clauses.
We call A ∨ B their resolvent.
¬P ∨ A P ∨ B
A ∨ B
both true
this true ← the resolvent
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 19 / 27
Propositional Resolution Generally
Let C1 and C2 be clauses such that P ∈ C1 and ¬P ∈ C2.
(C1 \ {P}) ∪ (C2 \ {¬P}) is a resolvent of C1 and C2.
(Note: A \B is set difference: the set of elements in A but not in B .)
Theorem. If R is a resolvent of C1 and C2 then C1 ∧ C2 |= R .
This generalises the well-known inference rule of modus ponens:
From A and A⇒ B deduce B .
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 20 / 27
Refuting a Set of Clauses
Resolution suggests a way of verifying that a CNF formula is
unsatisfiable.
¬P ∨ A P ∨ B
A ∨ B
conjunction false
this false ← the resolvent
If, through a number of resolution steps, we can derive the empty
clause ⊥, then the original set of clauses were unsatisfiable.
We talk about a refutation proof.
Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 21 / 27
Deductions and Refutations
A resolution deduction of clause C from a set S of clauses is a finite
sequence C1,C2, . . . ,Cn of clauses such that Cn = C and for each i ,
1 ≤ i ≤ n, Ci is either
a member of S , or
a resolvent of Cj and Ck , for some j , k < i . A resolution refutation of a set S of clauses is a resolution deduction of ⊥ from S . Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 22 / 27 An Example of a Refutation B ∨ ¬A B ∨ A ¬B A B ⊥ This shows that (B ∨ ¬A) ∧ (B ∨ A) ∧ ¬B is unsatisfiable. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 23 / 27 An Example of a Refutation B ∨ ¬A B ∨ A ¬B A B ⊥ This shows that (B ∨ ¬A) ∧ (B ∨ A) ∧ ¬B is unsatisfiable. Exercise: Find a simpler refutation to show the formula is a contradiction. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 23 / 27 Refutation Exercise Seek a resolution refutation of (A ∨ B) ∧ (¬A ∨ ¬B) A ∨ B ¬A ∨ ¬B ? Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 24 / 27 Refutation Exercise Seek a resolution refutation of (A ∨ B) ∧ (¬A ∨ ¬B) A ∨ B ¬A ∨ ¬B ? Not possible to derive ⊥ here —which is fortunate, because the original formula is satisfiable. Note in particular that we cannot “cancel out” several literals in one go. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 24 / 27 How to Use Refutations (1) To show that F is valid, first put ¬F in RCNF, yielding a set S of clauses. Then refute S , that is, deduce ⊥ from S . Consider: (P ⇒ R) ∨ (R ⇒ (P ∧ Q)) Negating yields: ¬((¬P ∨ R) ∨ (¬R ∨ (P ∧ Q))) Pushing negation then yields: P ∧ ¬R ∧ R ∧ (¬P ∨ ¬Q) From this we can derive ⊥ in a single resolution step. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 25 / 27 How to Use Refutations (2) Suppose we express a circuit design as a formula F in RCNF. Suppose we wish to show that the design satisfies some property G , that is, show F |= G . We can exploit this fact: F |= G iff F ∧ ¬G is unsatisfiable Hence a strategy is: 1 Negate G and bring it into RCNF; 2 add those clauses to the set F ; and 3 find a refutation of the resulting set of clauses. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 26 / 27 After the Break We move on to predicate logic. Grok Worksheet 1 (assessed) opened yesterday. It has a deadline of 22 August. Remember: No extensions are possible. Models of Computation (Sem 2, 2021) Symbolic Deduction c© University of Melbourne 27 / 27