Functional completeness.html (5165B)
1 <?xml version="1.0" encoding="UTF-8"?> 2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> 3 <html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-0.05603253096342087"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-20 14:35:25 +0000"/><meta name="latitude" content="52.33317063856025"/><meta name="longitude" content="4.865527388414661"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-20 16:17:14 +0000"/><title>Functional completeness</title></head><body><div>functionally complete — every truth table can be represented by a propositional formula (and vice versa)</div><div><br/></div><div><img src="Functional%20completeness.resources/screenshot.png" height="474" width="702"/><br/></div><div><br/></div><div><span style="font-weight: bold;">Disjunctive normal form (DNF)</span></div><div>this results in a disjunctive normal form (DNF, terms combined with disjunctions)</div><div>a DNF is a clause (disjunction of literals)</div><div><br/></div><div>a DNF is of the form:</div><div><br/></div><div>Ψ<span style="vertical-align: sub;">1</span> ∨ Ψ<span style="vertical-align: sub;">2</span> ∨ … ∨ Ψ<span style="vertical-align: sub;">n</span></div><div><br/></div><div>where Ψ<span style="vertical-align: sub;">i</span> is conjunctions of literals (p, ¬p, etc.)</div><div>a single letter is also a DNF</div><div><br/></div><div><span style="font-weight: bold;">Conjunctive normal form (CNF)</span></div><div>a conjunctive normal form (CNF) is conjunction Ψ<span style="vertical-align: sub; font-size: smaller; font-size: smaller;">1</span> ∧ Ψ<span style="vertical-align: sub; font-size: smaller; font-size: 11.666666030883789px;">2</span><span style="font-size: 11.666666030883789px;"> </span><span style="font-size: 14px;">∧ … ∧ Ψ</span><span style="font-size: smaller; vertical-align: sub; font-size: smaller;">n </span><span style="font-size: 14px;">where Ψ</span><span style="font-size: smaller; vertical-align: sub; font-size: smaller;">i</span><span style="font-size: 14px;"> are disjunctions of literals</span></div><div><span style="font-size: 14px;">disjunctions of literals are clauses (DNF), a CNF is a conjunction of clauses</span></div><div><span style="font-size: 14px;"><br/></span></div><div><img src="Functional%20completeness.resources/screenshot_1.png" height="390" width="601"/></div><div><br/></div><div>Transform any ϕ to CNF using algorithm in three easy steps</div><div><ol><li>IMPL-FREE: eliminate implications</li></ol></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div>ϕ ➝ Ψ ≡ ¬ ϕ ∨ Ψ </div></div></blockquote><div><ol start="2"><li>NNF: bring occurrences of ¬ inside, until directly in front of variable (removing double nots)</li></ol></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div>¬ (ϕ ∧ Ψ) ≡ ¬ ϕ ∨ ¬ Ψ</div></div><div>¬ (ϕ ∨ Ψ) ≡ ¬ ϕ ∧ ¬ Ψ</div><div>¬ ¬ ϕ ≡ ϕ</div></blockquote><div><div><ol start="3"><li>DISTR: use distributivity law to rearrange conj/disj</li></ol></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div><div>ϕ ∨ (Ψ ∧ Χ) ≡ (ϕ ∨ Ψ) ∧ (ϕ ∨ Χ)</div></div></div><div>(ϕ ∧ Ψ) ∨ Χ ≡ (ϕ ∨ Χ) ∧ (Ψ ∨ Χ)</div></blockquote><div><ol/></div><ol/><div><br/></div><div>Is a CNF Ψ<sub>1</sub> ∧ Ψ<sub>2</sub> ∧ … ∧ Ψ<sub>n</sub> a tautology?</div><div>Yes, only if in each of clauses Ψ<sub>i</sub> it contains literals p and ¬p for some variable p.</div><div><br/></div><div><b>Satisfiability problem</b></div><div>given a propositional formula ϕ, find a valuation that applied to ϕ yields T.</div><div>NP-complete — no efficient solution has been found</div><div><br/></div><div>DPLL (Davis-Putnam-Logemann-Loveland) procedure:</div><div>checks satisfiability of formula ϕ in CNF.</div><div>T — constant true</div><div>_|_ — constant false</div><div><br/></div><div>applies reduction rules:</div><div><img src="Functional%20completeness.resources/screenshot_2.png" height="161" width="600"/></div><div><br/></div><div>To check satisfiability of CNF ϕ:</div><div><ol><li>Eliminate “unit” clauses</li><ul><li>for clause p of ϕ, replace p in ϕ by T</li><li>for clause ¬ p of ϕ, replace p in ϕ by _|_</li></ul><li>Eliminate “pure” propositional variables</li><ul><li>if p only occurs positively in ϕ, replace all p in ϕ by T</li><li>if p only occurs negatively in ϕ, replace all p in ϕ by _|_</li></ul><li>If ϕ is T, it is satisfiable</li><li>If ϕ is _|_, it is unsatisfiable</li><li>Choose a p in ϕ:</li><ul><li>replace all p in ϕ by T, apply DPLL</li><li>if outcome is “unsatisfiable, replace all p in ϕ by _|_ and apply DPLL again<br/></li></ul></ol></div><div><br/></div></body></html>