Logic: Resolution Inference Rule

# Logic: Resolution Inference Rule **Video Category:** Computer Science / Artificial Intelligence Tutorial ## 📋 0. Video Metadata **Video Title:** Logic: resolution **YouTube Channel:** Stanford ENGINEERING **Publication Date:** Not shown in video **Video Duration:** ~19 minutes ## 📝 1. Core Summary (TL;DR) This video introduces "resolution," a powerful inference rule in propositional logic designed to overcome the incompleteness of Modus Ponens. While Modus Ponens is only complete for a restricted subset of logic (Horn clauses), resolution is both sound and complete for *all* of propositional logic. It works by converting any logical formula into Conjunctive Normal Form (CNF) and systematically canceling out contradictory literals to derive new truths or prove contradictions. However, this universal expressiveness comes with a significant computational cost, requiring exponential time in the worst-case scenario. ## 2. Core Concepts & Frameworks * **Inference Rule:** -> **Meaning:** A purely syntactic manipulation of logical formulas to derive or prove new formulas without needing to enumerate all possible models (truth tables). -> **Application:** Used in automated theorem proving to programmatically deduce consequences from a knowledge base. * **Soundness & Completeness:** -> **Meaning:** An inference rule is *sound* if everything it derives is actually true (no false positives). It is *complete* if it can derive all formulas that are true (no false negatives). -> **Application:** Modus Ponens is sound but incomplete for general logic; Resolution is both sound and complete for general propositional logic. * **Literal & Clause:** -> **Meaning:** A *literal* is a single propositional symbol ($p$) or its negation ($\neg p$). A *clause* is a disjunction (an "OR" statement, $\vee$) of multiple literals (e.g., $p_1 \vee \neg p_2 \vee p_3$). -> **Application:** These are the atomic building blocks required for the resolution algorithm. * **Horn Clause:** -> **Meaning:** A specific type of clause that contains *at most one positive literal*. -> **Application:** If a knowledge base is restricted entirely to Horn clauses, Modus Ponens can be used to achieve completeness in linear time. * **Conjunctive Normal Form (CNF):** -> **Meaning:** A standardized logical format consisting of a conjunction (an "AND" statement, $\wedge$) of multiple clauses. -> **Application:** Every formula in propositional logic must be converted into CNF before the resolution inference rule can be applied to it. * **The Resolution Inference Rule:** -> **Meaning:** If you have two clauses where one contains a positive literal ($P$) and the other contains the corresponding negative literal ($\neg P$), you can cancel them out and combine the remaining literals into a new valid clause. -> **Application:** Used iteratively to combine facts in a knowledge base to eventually derive a target formula or a contradiction. ## 3. Evidence & Examples (Hyper-Specific Details) * **Logical Equivalences (De Morgan's Laws):** The speaker manually writes out equivalences crucial for CNF conversion: * Implication elimination: $p \rightarrow q \equiv \neg p \vee q$ * De Morgan's 1: $\neg(p \wedge q) \equiv \neg p \vee \neg q$ * De Morgan's 2: $\neg(p \vee q) \equiv \neg p \wedge \neg q$ * **Horn Clause vs. General Clause Demonstration:** * **Not a Horn Clause:** $P_1 \vee \neg P_2 \vee P_3$ (Fails the rule because it contains two positive literals: $P_1$ and $P_3$). * **Valid Horn Clause:** $P_1 \vee \neg P_2 \vee \neg P_3$ (Passes because it contains exactly one positive literal: $P_1$). * **Modus Ponens Expressed as Resolution:** * Modus Ponens states: $A$, and $A \rightarrow C$, therefore $C$. * Converted to clauses: $A$ is one clause. $A \rightarrow C$ becomes $\neg A \vee C$. * Resolution step: The positive $A$ and the negative $\neg A$ cancel out, leaving exactly $C$. * **General Resolution Example (Rain/Snow/Traffic):** * Clause 1: $Rain \vee Snow$ * Clause 2: $\neg Snow \vee Traffic$ * Resolution step: The $Snow$ and $\neg Snow$ terms are canceled. * Conclusion: $Rain \vee Traffic$. * **Intuitive reasoning:** If it's snowing, Clause 2 requires Traffic to be true. If it's not snowing, Clause 1 requires Rain to be true. Therefore, regardless of whether it is snowing or not, it must either be Raining or there is Traffic. * **Visual Proof of Soundness (Model Intersection):** The video demonstrates soundness by showing that the models of the premise are a subset of the models of the conclusion. * A truth table for 3 variables (Snow, Rain, Traffic) generates 8 possible models. * Models for $(Rain \vee Snow) \wedge (\neg Snow \vee Traffic)$ are identified (dark red squares on the slide). * Models for the conclusion $(Rain \vee Traffic)$ are identified (green squares). * Because all dark red squares fall inside the green squares, the inference is proven sound ($M(KB) \subseteq M(f)$). * **Step-by-Step CNF Conversion Example:** * Initial Formula: $(Summer \rightarrow Snow) \rightarrow Bizarre$ * Step 1 (Remove implication): $\neg(\neg Summer \vee Snow) \vee Bizarre$ * Step 2 (Push negation inwards via De Morgan's): $(Summer \wedge \neg Snow) \vee Bizarre$ * Step 3 (Distribute $\vee$ over $\wedge$): $(Summer \vee Bizarre) \wedge (\neg Snow \vee Bizarre)$ * **Resolution Algorithm Execution (Proof by Contradiction):** * **Initial KB:** $\{A \rightarrow (B \vee C), A, \neg B\}$ * **Query ($f$):** Does KB entail $C$? * **Step 1:** Add $\neg f$ to KB -> $KB' = \{A \rightarrow (B \vee C), A, \neg B, \neg C\}$ * **Step 2:** Convert to CNF -> $KB' = \{\neg A \vee B \vee C, A, \neg B, \neg C\}$ * **Step 3 (Resolve):** Resolve $A$ with $\neg A \vee B \vee C$ -> yields $B \vee C$ * **Step 4 (Resolve):** Resolve $\neg B$ with $B \vee C$ -> yields $C$ * **Step 5 (Resolve):** Resolve $\neg C$ with newly derived $C$ -> yields 'false' (empty clause). * **Result:** Because deriving 'false' indicates $KB \cup \{\neg f\}$ is unsatisfiable, the original KB successfully entails $C$. ## 4. Actionable Takeaways (Implementation Rules) * **Rule 1: Convert all knowledge to CNF before running inference** - You cannot apply resolution to raw logical statements containing implications or un-distributed ANDs. You must strictly follow the conversion recipe: eliminate bidirectional implications ($\leftrightarrow$), eliminate standard implications ($\rightarrow$), push negations inward using De Morgan's laws, remove double negations, and distribute ORs over ANDs until every formula is a conjunction of clauses. * **Rule 2: Use "Proof by Contradiction" to automate theorem proving** - To ask an AI system if a knowledge base (KB) entails a specific fact ($f$), do not try to build $f$ from scratch. Instead, negate the fact ($\neg f$), add it to the KB, and run the resolution algorithm. If the algorithm eventually derives an empty clause ("false"), the original fact $f$ is guaranteed to be true. * **Rule 3: Match the logic subset to your performance constraints** - If your application requires real-time or rapid inference, you must restrict your knowledge base strictly to Horn clauses so you can use Modus Ponens, which operates in linear time. * **Rule 4: Accept exponential time costs for full expressiveness** - If your application requires complex logic (e.g., general clauses with multiple positive literals), you must use the Resolution rule. However, you must design your system anticipating exponential worst-case time complexity, as general resolution is equivalent to solving the NP-complete SAT problem. ## 5. Pitfalls & Limitations (Anti-Patterns) * **Pitfall: Relying on Modus Ponens for general propositional logic.** -> **Why it fails:** Modus Ponens is incomplete outside of Horn clauses. It will simply fail to deduce true statements if the required knowledge relies on general disjunctions. -> **Warning sign:** An AI agent fails to answer queries correctly despite the necessary information theoretically existing in its knowledge base. * **Pitfall: Attempting resolution on non-clausal forms.** -> **Why it fails:** The syntactic cancellation mechanism of resolution (canceling $P$ and $\neg P$) is mathematically invalid if the terms are nested inside implications or conjunctions. -> **Warning sign:** Generating nonsense derivations or false proofs during the syntactic manipulation step. * **Pitfall: Unbounded computational explosion.** -> **Why it fails:** The resolution algorithm systematically adds new clauses to the knowledge base by combining existing ones. In the worst case, it must explore all possible subsets of symbols, leading to exponential time and memory consumption. -> **Warning sign:** The theorem prover hangs, slows to a crawl, or crashes with out-of-memory errors when the knowledge base grows even moderately in size. ## 6. Key Quote / Core Insight "If you want the full expressiveness to represent any propositional formula, you must use the resolution rule, but this power inherently comes at the cost of exponential time complexity—highlighting the fundamental trade-off in AI between how much you can say and how fast you can reason about it." ## 7. Additional Resources & References * **Resource:** Resolution [Robinson, 1965] - **Type:** Academic Paper / Theoretical Framework - **Relevance:** The foundational reference cited in the slide for the invention of the general resolution inference rule.