CS代写 CS262 Logic and Verification Lecture 3: Boolean algebra

CS262 Logic and Verification Lecture 3: Boolean algebra
CS262 Logic and Verification 1 / 7

Logical equivalence

Copyright By PowCoder代写 加微信 powcoder

Formulas are truth functions: each valuation maps the formula to T or F. Formulas representing the same truth function are called logically
equivalent. Example:
p q p→q ¬p ∨ q TTTFT TFFFF FTTTT FFTTT
Wewrite: p→q=¬p∨q
We can replace logically equivalent formulas by each other. This also works for compound formulas: X → Y = ¬X ∨ Y
CS262 Logic and Verification

Laws of Boolean algebra
X ∨X =X X ∧X =X X = ¬¬X
X → Y = ¬X ∨ Y
X ∧Y =Y ∧X
Idempotence Double negation Replacing implication Commutativity Associativity
De Morgan’s Laws Distributivity
Exportation Absorption Law Contradiction Neutral elements
X ∨Y =Y ∨X (X ∧ Y ) ∧ Z = X ∧ (Y ∧ Z )
(X ∨ Y ) ∨ Z = X ∨ (Y ∨ Z )
¬(X ∨Y)=¬X ∧¬Y
¬(X ∧ Y ) = ¬X ∨ ¬Y
X ∧(Y ∨Z)=(X ∧Y)∨(X ∧Z) X ∨ (Y ∧ Z ) = (X ∨ Y ) ∧ (X ∨ Z ) (X ∧ Y ) → Z = X → (Y → Z )
X → Y = X → (X ∧ Y )
(X →Y)∧(X →¬Y)=¬X X ∨⊤=⊤ X ∧⊤=X X∨⊥=X X∧⊥=⊥
X ∨ ¬X = ⊤ X ∧ ¬X = ⊥
and many more…
CS262 Logic and Verification

These laws can be verified by truth tables, or by deriving them from other laws.
Example: (X → Y ) ∧ (X → ¬Y ) = ¬X (contradiction law)
(X → Y ) ∧ (X → ¬Y ) (replace implication) = (¬X ∨ Y ) ∧ (¬X ∨ ¬Y ) (distributivity)
= ¬X ∨ (Y ∧ ¬Y ) (neutral elements)
= ¬X ∨ ⊥ (neutral elements)
CS262 Logic and Verification

Rewriting/simplifying formulas
Laws of Boolean algebra can be used to simplify complex formulas.
􏰀(p ∧ q) → (r ∧ s)􏰁 ∨ (p ∧ q) (replace implication) = 􏰀¬(p ∧ q) ∨ (r ∧ s)􏰁 ∨ (p ∧ q) (commutativity) = 􏰀(r ∧ s) ∨ ¬(p ∧ q)􏰁 ∨ (p ∧ q) (associativity) =(r∧s)∨􏰀¬(p∧q)∨(p∧q)􏰁 (neutralelements) = (r ∧ s) ∨ ⊤ (neutral elements)
This is called equational reasoning.
Problem: It is difficult to automate. Which rule to apply next?
CS262 Logic and Verification

Prove the following useful equivalences (by equational reasoning using the aforementioned laws):
X → Y = ¬Y → ¬X
(X∨Y)→Z =(X→Z)∧(Y→Z) X →(Y ∧Z) = (X →Y)∧(X →Z)
CS262 Logic and Verification 6 / 7

Getting rid of logical operators
We know that X → Y = ¬X ∨Y, so any occurence of → can be replaced. Hence → is not strictly necessary in our language.
Question: What is a small/minimal set of connectives that allows us to express any Boolean function?
This will be discussed in the exercises.
CS262 Logic and Verification 7 / 7

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com