1CS157 Greatest HitsThe Top 100 Slides of the CourseComputational Logic Lecture 19Michael Genesereth Autumn 200512/6/05 2SyntaxPropositional Constants: raining, snowing, cloudyNegations: ¬rainingConjunctions: (raining ∧ snowing)Disjunctions: (raining ∨ snowing)Implications: (raining ⇒ cloudy)Reductions: (cloudy ⇐ raining)Equivalences: (cloudy ⇔ raining)Nesting: ((raining ∨ snowing) ⇒ cloudy)212/6/05 3Propositional InterpretationA propositional interpretation is an associationbetween the propositional constants in a propositionallanguage and the truth values T or F.pi → T pi= Tqi → F qi= Fri → T ri= T12/6/05 4Sentential InterpretationA sentential interpretation is an association betweenthe sentences in a propositional language and the truthvalues T or F.pi = T (p ∨ q)i = Tqi = F (¬q ∨ r)i = Tri = T ((p ∨ q) ∧ (¬q ∨ r))i = TA propositional interpretation defines a sententialinterpretation by application of operator semantics.312/6/05 5Operator Semanticsφ¬φT FF Tφ ψ φ∧ψT T TT F FF T FF F Fφ ψ φ∨ψT T TT F TF T TF F Fφ ψ φ⇔ψT T TT F FF T FF F Tφ ψ φ⇒ψT T TT F FF T TF F Tφ ψ φ⇐ψT T TT F TF T FF F T12/6/05 6EvaluationInterpretation i:Compound Sentence(p ∨ q) ∧ (¬q ∨ r)pi= Tqi= Fri= T412/6/05 7Truth Tables€ p q rT T TT T FT F TT F FF T TF T FF F TF F FA truth table is a table of all possible interpretationsfor the propositional constants in a language.One column per constant.One row per interpretation.For a language with n constants,there are 2n interpretations.12/6/05 8Properties of SentencesA sentence is valid if and only ifevery interpretation satisfies it.A sentence is contingent if and only ifsome interpretation satisfies it andsome interpretation falsifies it.A sentence is unsatisfiable if andonly if no interpretation satisfies it.ValidContingentUnsatisfiable512/6/05 9Properties of SentencesA sentences is satisfiable if and onlyif it is either valid or contingent.A sentences is falsifiable if and onlyif it is contingent or unsatisfiable.ValidContingentUnsatisfiable}}12/6/05 10Evaluation Versus SatisfactionEvaluation:Satisfaction:pi= Tqi= F( p ∨ q)i= T(¬q)i= T( p ∨ q)i= T(¬q)i= Tpi= Tqi= F612/6/05 11Logical EntailmentA set of premises Δ logically entails a conclusion ϕ(written as Δ |= ϕ) if and only if every interpretationthat satisfies the premises also satisfies theconclusion.{p} |= (p ∨ q){p} |# (p ∧ q){p, q} |= (p ∧ q)12/6/05 12Proof (Official Version)A proof of a conclusion from a set of premises is asequence of sentences terminating in the conclusionin which each item is either:1. a premise2. An instance of an axiom schema3. the result of applying a rule of inference to earlieritems in sequence.712/6/05 13ProvabilityA conclusion is said to be provable from a set ofpremises (written Δ |- ϕ) if and only if there is a finiteproof of the conclusion from the premises using onlyModus Ponens and the Standard Axiom Schemata.12/6/05 14Soundness and CompletenessSoundness: Our proof system is sound, i.e. if theconclusion is provable from the premises, then thepremises propositionally entail the conclusion.(Δ |- ϕ) ⇒ (Δ |= ϕ)Completeness: Our proof system is complete, i.e. if thepremises propositionally entail the conclusion, then theconclusion is provable from the premises.(Δ |= ϕ) ⇒ (Δ |- ϕ)812/6/05 15MetatheoremsDeduction Theorem: Δ |- (ϕ ⇒ ψ) if and only ifΔ∪{ϕ} |- ψ.Equivalence Theorem: Δ |- (ϕ ⇔ ψ) and Δ |- χ, then itis the case that Δ !|- χϕ←ψ.12/6/05 16Clausal FormA literal is either an atomic sentence or a negation ofan atomic sentence.p, ¬pA clausal sentence is either a literal or a disjunctionof literals.p, ¬p, p ∨ qA clause is a set of literals.!{p}, {¬p}, {p,q}912/6/05 17Conversion to Clausal Formϕ1⇒ϕ2→ ¬ϕ1∨ϕ2ϕ1⇐ϕ2→ϕ1∨ ¬ϕ2ϕ1⇔ϕ2→ (¬ϕ1∨ϕ2) ∧ (ϕ1∨ ¬ϕ2)¬¬ϕ→ϕ¬(ϕ1∧ϕ2) → ¬ϕ1∨ ¬ϕ2¬(ϕ1∨ϕ2) → ¬ϕ1∧ ¬ϕ2Implications Out:Negations In:12/6/05 18Conversion to Clausal FormDistributionOperators Outϕ1∨ (ϕ2∧ϕ3) → (ϕ1∨ϕ2) ∧ (ϕ1∨ϕn)(ϕ1∧ϕ2) ∨ϕ3→ (ϕ1∨ϕ3) ∧ (ϕ2∨ϕ3)ϕ1∨ (ϕ2∨ϕ3) → (ϕ1∨ϕ2∨ϕ3)(ϕ1∨ϕ2) ∨ϕ3→ (ϕ1∨ϕ2∨ϕ3)ϕ1∧ (ϕ2∧ϕ3) → (ϕ1∧ϕ2∧ϕ3)(ϕ1∧ϕ2) ∧ϕ3→ (ϕ1∧ϕ2∧ϕ3)ϕ1∨ ... ∨ϕn→ {ϕ1,...,ϕn}ϕ1∧... ∧ϕn→ϕ1,...,ϕn1012/6/05 19Resolution PrincipleGeneral:Example:{ϕ1,...,χ,...,ϕm}{ψ1,..., ¬χ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}{p,q}{¬p, r}{q, r}12/6/05 20Soundness and CompletenessA sentence is provable from a set of sentences bypropositional resolution if and only if there is aderivation of the empty clause from the clausal formof Δ∪{¬ϕ}.Theorem: Propositional Resolution is sound andcomplete, i.e. Δ |= ϕ if and only if Δ |- ϕ.1112/6/05 21Davis Putnam Procedurefunction dp (Δ) {for ϕ in vocabulary(Δ) do {var Δ’←{}; for Φ1 in Δ for Φ2 in Δ such that ϕ ∈ Φ1 ¬ϕ ∈ Φ2 do {var Φ’← Φ1− {ϕ} ∪ Φ2 − {¬ϕ}; if not tautology(Φ’) then Δ’←Δ’∪{Φ’}}; Δ←Δ − {Φ∈Δ | ϕ ∈ Φ or ¬ϕ ∈ Φ} ∪ Δ’}; return {if {} ∈ Δ then unsatisfiable else satisfiable}}function tautology(Φ) {ϕ∈ Φ and ¬ϕ ∈ Φ}12/6/05 22Davis-Putnam Example{p, q, r} {q, r}{p, q, ¬r} {q, ¬r}{p, ¬q, r} {¬q, r}{p, ¬q, ¬r} {¬q, ¬r}{¬p, q, r}{¬p, q, ¬r} {r}{¬p, ¬q, r} {¬r}{¬p, ¬q, ¬r}{}Cost = 16 + 4 + 1 = 21 resolutions1212/6/05 23Davis Putnam Logemann Lovelandfunction dpll (Δ) {var ϕ; if Δ = {} then return yes; if {}∈ Δ then return no; ϕ ← choose vocabulary(Δ)); if dpll(simplify(Δ, ϕ)) return yes else return dpll(simplify(Δ,¬ϕ))}12/6/05 24Simplificationfunction simplify (Δ, ϕ) {var Δ’; for Φ ∈ Δ do {if ϕ∈Φ then skip else if negation(ϕ)∈Φ then Δ’← Δ’ ∪ {Φ − {negation(ϕ)}} else Δ’← Δ’ ∪ {Φ}}}Example:simplify ({{p,q},{¬p,r},{¬r,s}}, p) = {{r},{¬r,s}}1312/6/05 2512/6/05 26WordsVariables begin with characters from the end of thealphabet (from u through z).Constants begin with digits or letters from thebeginning of the alphabet (from a through t).Object constants refer to objects.Function constants denote functions.Relation constants refer to relations.There is no syntactic distinction between object,function, and relation constants. The type of eachsuch word is determined from context.1412/6/05 27Functional TermsA functional term is
View Full Document
Unlocking...