CS262 Logic and Verification Lecture 5: Normal form algorithms
CS262 Logic and Verification 1 / 17
Generalized disjunctions/conjunctions
Copyright By PowCoder代写 加微信 powcoder
Let X1, X2, . . . , Xn be a sequence of propositional formulas. We write a generalized disjunction as:
[X1, X2, . . . , Xn] := X1 ∨ X2 ∨ · · · ∨ Xn (recall associativity!)
We write a generalized conjunction as: ⟨X1,X2,…,Xn⟩:=X1 ∧X2 ∧···∧Xn
If X1,…,Xn are literals, then [X1,X2,…,Xn] is called a clause, and ⟨X1, X2, . . . , Xn⟩ is called a dual clause.
CS262 Logic and Verification
Valuations on generalized disjunctions/disjunctions
This is how valuations act on generalized disjunctions/disjunctions: v([X1,…,Xn]) = T if and only if v(Xi) = T for at least one member of
the list X1,…,Xn.
v(⟨X1,…,Xn⟩) = T if and only if v(Xi) = T for every member of the
list X1,…,Xn.
v ([ ]) = v (⊥) = F (neutral element of disjunction) v (⟨ ⟩) = v (⊤) = T (neutral element of conjunction)
CS262 Logic and Verification
α- and β-formulas
We group all propositional formulas of the forms (X ◦ Y ) and ¬(X ◦ Y ) (where ◦ is one of {∧, ∨, →, ←, ↑, ↓, ̸→, ̸←}, see the exercises) into two categories, those that act conjunctively, and those that act disjunctively:
Conjunctive Disjunctive
α β1 β2 X∧Y X Y ¬(X∧Y) ¬X ¬Y
¬(X∨Y) ¬X ¬Y X∨Y X Y ¬(X→Y) X ¬Y X→Y ¬X Y ¬(X←Y)¬XY X←Y X¬Y
¬(X↑Y) X Y X↑Y ¬X ¬Y X↓Y ¬X ¬Y ¬(X↓Y) X Y X ̸→ Y X ¬Y ¬(X ̸→ Y ) ¬X Y
X ̸← Y ¬X Y ¬(X ̸← Y ) X ¬Y
CS262 Logic and Verification
Valuations on α- and β-formulas
For every α- and β-formula and every valuation v, we have v(α) = v(α1) ∧ v(α2)
v(β) = v(β1) ∨ v(β2)
I.e., we have α = α1 ∧ α2 and β = β1 ∨ β2 (logical equivalence).
CS262 Logic and Verification 5 / 17
Conjunctive normal form algorithm
Given any any propositional formula X, start with ⟨[X]⟩.
Given the current expansion ⟨D1 , . . . , Dn ⟩, select one of the disjunctions Di
that is not a disjunction of literals.
Select a non-literal N from Di .
If N = ¬⊤, then replace N by ⊥.
If N = ¬⊥, then replace N by ⊤.
If N = ¬¬Z, then replace N by Z.
If N is a β-formula, then replace N by the two formula sequence β1,β2 (β-expansion).
If N is an α-formula, then replace the disjunction Di with two disjunctions, one in which N is replaced by α1, and one in which N is replaced by α2 (α-expansion).
CS262 Logic and Verification 6 / 17
Example 1 (CNF expansion)
¬(p ∧ ¬⊥) ∨ ¬(⊤ ↑ q)
[¬(p ∧ ¬⊥) ∨ ¬(⊤ ↑ q)] = . . .
CS262 Logic and Verification 7 / 17
Example 2 (CNF expansion)
(¬p → (q ̸← r)) → ((p ↓ q) ↑ (p → ¬r))
[(¬p → (q ̸← r)) → ((p ↓ q) ↑ (p → ¬r))] = …
CS262 Logic and Verification 8 / 17
CNF algorithm expansion rules
Here is a compact representation of these rules:
¬⊤ ¬⊥ ¬¬Z β α ⊥ ⊤ Z β1 α1|α2
CS262 Logic and Verification 9 / 17
Correctness of this algorithm
Proposition: Throughout the algorithm, we produce a sequence of logically equivalent formulas.
Proof: We only verify the last two steps.
β-expansion:
Di = [β,X2,…,Xk] =[β1 ∨β2,X2,…,Xk] = [β1,β2,X2,…,Xk]
α-expansion:
Di = [α,X2,…,Xk]
=(α1 ∧α2)∨(X2 ∨···∨Xk)
=(α1 ∨(X2 ∨···∨Xk))∧(α2 ∨(X2 ∨···∨Xk)) = ⟨[α1,X2,…,Xk],[α2,X2,…,Xk]⟩
CS262 Logic and Verification
Termination of the algorithm
Proposition: The algorithm terminates, regardless of which choices are made during the algorithm.
To prove this, we need to make a little detour.
Consider a rooted tree. A branch is a sequence of nodes starting at the root, descending towards one of the childen in each step (unless no children are present). We say that the tree is finitely branching, if every node has only finitely many children (possibly 0). A tree/branch is finite if it has a finite number of nodes; otherwise it is infinite.
Theorem (K ̈onig’s lemma): A tree that is finitely branching but infinite must have an infinite branch.
CS262 Logic and Verification 11 / 17
A game with balls
Consider the following game played with balls that have non-negative integer labels:
At the beginning, we have a box containing just one ball.
In each step, we may remove one ball from the box, and replace it by any (finite) number of balls having lower numbers.
Theorem: This game must end, regardless of which choices are made during the game.
Proof: Use K ̈onig’s theorem.
CS262 Logic and Verification 12 / 17
Termination of the algorithm
Proposition: The algorithm terminates, regardless of which choices are made during the algorithm.
Proof: Define the rank of a propositional formula as follows: Recursion anchor: r(p) = r(¬p) = 0 for variables p; r(⊤) = r(⊥) = 0;
r(¬⊤) = r(¬⊥) = 1.
Recursive step: r(¬¬Z) = r(Z) + 1;
r(α) = r(α1) + r(α2) + 1; r(β) = r(β1) + r(β2) + 1
For a generalized disjunction: r([X1,…,Xn]) = ni=1 r(Xi)
r ((p → ¬q) ∧ (¬¬r ∧ ¬⊥)) = . . . r ([p ∧ q, ¬⊤, ¬¬r ]) = . . .
Answers should be 5 and 3, respectively.
CS262 Logic and Verification
Termination of the algorithm
Proposition: The algorithm terminates, regardless of which choices are made during the algorithm.
Proof: …continued…
Assign the current conjunction of disjunctions ⟨D1 , . . . , Dn ⟩ a sequence of n balls, by placing one ball labelled r(Di) for each disjunction Di into a box.
Argue that each step of the algorithm corresponds to removing one ball from the box, and replacing it either by two balls with a lower number (α-expansion) or by one ball with a lower number (in all other cases).
Example: ⟨[p∧q,¬⊤,¬¬r],[p→q]⟩
We have argued before that this game must end, so our algorithm must terminate.
CS262 Logic and Verification
Normal form algorithms
We have seen an algorithm to transform any formula into conjunctive normal form (CNF). How to do the same for disjunctive normal form (DNF)?
Recall the CNF algorithm: Start with ⟨[X]⟩, and repeatedly apply one of the following expansion rules:
¬⊤ ¬⊥ ¬¬Z β α ⊥ ⊤ Z β1 α1|α2
Here is the DNF algorithm: Start with [⟨X⟩], and repeatedly apply one of
the following expansion rules:
¬⊤ ¬⊥ ¬¬Z β α ⊥ ⊤ Z β1|β2 α1 α2
CS262 Logic and Verification 15 / 17
Example 1 (DNF expansion)
¬(p ∧ ¬⊥) ∨ ¬(⊤ ↑ q)
⟨¬(p ∧ ¬⊥) ∨ ¬(⊤ ↑ q)⟩ = . . .
CS262 Logic and Verification 16 / 17
Example 2 (DNF expansion)
(¬p → (q ̸← r)) → ((p ↓ q) ↑ (p → ¬r))
⟨(¬p → (q ̸← r)) → ((p ↓ q) ↑ (p → ¬r))⟩ = …
CS262 Logic and Verification 17 / 17
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com