CS157 Greatest Hits The Top 100 Slides of the CourseSyntaxPropositional InterpretationSentential InterpretationOperator SemanticsEvaluationTruth TablesProperties of SentencesSlide 9Evaluation Versus SatisfactionLogical EntailmentProof (Official Version)ProvabilitySoundness and CompletenessMetatheoremsClausal FormConversion to Clausal FormSlide 18Resolution PrincipleSlide 20Davis Putnam ProcedureDavis-Putnam ExampleDavis Putnam Logemann LovelandSimplificationPowerPoint PresentationWordsFunctional TermsRelational SentencesLogical SentencesQuantified SentencesConceptualizationInterpretationsVariable AssignmentsValue AssignmentsTruth AssignmentsSlide 36Slide 37VersionsSlide 39HHHHerbrandHerbrand TheoremModus PonensUniversal GeneralizationStandard Axiom SchemataStandard Axiom Schemata (concluded)FreedomSubstitutabilityFormal ProofsSlide 49Decidability ResultsSlide 51InseadoInseado (continued)Slide 54Inseado (concluded)UnificationMost General UnifierRelational Resolution IRelational Resolution IIRelational Resolution III (Final Version)Slide 61Slide 62Answer Extraction MethodStrategiesClauses and ChainsOrdered ResolutionSemi-Ordered ResolutionContrapositivesModel EliminationNormal and Reduced LiteralsModel Elimination RulesEpilogRule FormBackward ChainingSlide 75EqualityExampleUnique Names AssumptionEquational ReasoningEquality AxiomsEquality Axioms in Rule FormEquality ProofEquality ProblemFlatteningProof With FlatteningSubstitution AxiomProof With SubstitutionNotesDemodulationExamplesNon-ExamplesProblems With DemodulationParamodulationSlide 94Proof With ParamodulationSlide 96DifferencesPowerDetailsHintsCS157 Greatest HitsThe Top 100 Slides of the CourseComputational Logic Lecture 19Michael Genesereth Autumn 200701/14/19 2SyntaxPropositional Constants: raining, snowing, cloudyNegations: rainingConjunctions: (raining snowing)Disjunctions: (raining snowing)Implications: (raining cloudy)Reductions: (cloudy raining)Equivalences: (cloudy raining)Nesting: ((raining snowing) cloudy)01/14/19 3Propositional InterpretationA propositional interpretation is an association between the propositional constants in a propositional language and the truth values T or F.pi ⏐ → ⏐ T pi=Tqi ⏐ → ⏐ F qi=Fri ⏐ → ⏐ T ri=T01/14/19 4Sentential InterpretationA sentential interpretation is an association between the sentences in a propositional language and the truth values 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 sentential interpretation by application of operator semantics.01/14/19 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 T01/14/19 6EvaluationInterpretation i:Compound Sentence(p q) (q r)pi= Tqi= Fri= T01/14/19 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.01/14/19 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.ValidContingentUnsatisfiable01/14/19 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.ValidContingentUnsatisfiable01/14/19 10Evaluation Versus SatisfactionEvaluation:Satisfaction:pi= Tqi= F(p∨q)i= T(¬q)i= T(p∨q)i= T(¬q)i= Tpi= Tqi= F01/14/19 11Logical EntailmentA set of premises logically entails a conclusion (written as |= ) if and only if every interpretation that satisfies the premises also satisfies the conclusion.{p} |= (p q){p} |# (p q){p, q} |= (p q)01/14/19 12Proof (Official Version)A proof of a conclusion from a set of premises is a sequence of sentences terminating in the conclusion in which each item is either:1. a premise2. An instance of an axiom schema3. the result of applying a rule of inference to earlier items in sequence.01/14/19 13ProvabilityA conclusion is said to be provable from a set of premises (written |- ) if and only if there is a finite proof of the conclusion from the premises using only Modus Ponens and the Standard Axiom Schemata.01/14/19 14Soundness and CompletenessSoundness: Our proof system is sound, i.e. if the conclusion is provable from the premises, then the premises propositionally entail the conclusion.( |- ) ( |= ) Completeness: Our proof system is complete, i.e. if the premises propositionally entail the conclusion, then the conclusion is provable from the premises.( |= ) ( |- )01/14/19 15MetatheoremsDeduction Theorem: |- ( ) if and only if {} |- .Equivalence Theorem: |- ( ) and |- , then it is the case that |- .01/14/19 16Clausal FormA literal is either an atomic sentence or a negation of an atomic sentence.p, pA clausal sentence is either a literal or a disjunction of literals.p, p, p qA clause is a set of literals.{p}, {p}, {p,q}01/14/19 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:01/14/19 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,...,ϕn01/14/19 19Resolution PrincipleGeneral:Example:{ϕ1,...,χ,...,ϕm}{ψ1,...,¬χ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}{p,q}{¬p,r}{q,r}01/14/19 20Soundness and CompletenessA sentence is provable from a set of sentences by propositional resolution if and only if there is a derivation of the empty clause from the clausal form of {}.Theorem: Propositional Resolution is
View Full Document
Unlocking...