Propositional Logic: Entailment, CNF & Forward/Backward Chaining
“Logical entailment KB |= alpha, CNF conversion, Horn clauses, and linear-time chaining algorithms.”
1.Propositional Logic: Syntax, Models & Entailment
§ 4.1.Propositional logic provides formal language for knowledge representation:
• Syntax: Propositional symbols (P, Q, R) connected by Boolean connectives (\neg, \land, \lor, \implies, \iff).
• Models: A model m is a complete assignment of truth values (True/False) to every propositional symbol. With n symbols, there are exactly 2^n distinct models.
• Entailment (KB \models \alpha): Knowledge Base KB entails sentence \alpha if and only if \alpha is true in every model in which KB is true (M(KB) \subseteq M(\alpha)).
Theorem: KB \models \alpha \iff (KB \land \neg \alpha) is unsatisfiable. This fundamental equivalence forms the foundation of all resolution refutation automated theorem provers.
2.Horn Clauses & Linear-Time Chaining Algorithms
§ 4.2.While general Boolean satisfiability (SAT) is NP-Complete, restricting knowledge bases to Definite Clauses enables inference in linear O(n) time.
Definitions:
• Definite Clause: A disjunction of literals with exactly one positive literal: (\neg P_1 \lor \neg P_2 \lor ... \lor \neg P_k \lor Q) \equiv (P_1 \land P_2 \land ... \land P_k) \implies Q.
• Horn Clause: A disjunction of literals with at most one positive literal.
Algorithms for Definite Clause Knowledge Bases:
1. Forward Chaining (Data-Driven): Starts with known atomic facts. Whenever all premises of an implication (P_1 \land P_2) \implies Q are satisfied, rule fires and adds Q to the known database. Continues until query is generated or no new facts appear. Runs in linear O(n) time with respect to the size of KB.
2. Backward Chaining (Goal-Directed): Starts from the query goal Q. Searches for rules having Q as conclusion, and recursively proves each of their premises. Ideal for interactive diagnostics.
3. GATE Worked Numerical: CNF Conversion Pipeline
Distribute OR over AND carefully: (A and B) or C becomes (A or C) and (B or C)!
Problem (Original Practice Problem · Modeled on GATE DA Pattern):
Convert the propositional sentence S = (P or Q) -> (R and S) into Conjunctive Normal Form (CNF).
Step 1: Eliminate Implication (A -> B = ~A or B):
S = ~((P or Q)) or (R and S).
Step 2: Apply De Morgan's Law to move negation inward:
~((P or Q)) = (~P and ~Q).
Sentence becomes: (~P and ~Q) or (R and S).
Step 3: Distribute OR over AND:
Let X = (~P and ~Q). We have X or (R and S) = (X or R) and (X or S).
Expand (X or R) = ((~P and ~Q) or R) = (~P or R) and (~Q or R).
Expand (X or S) = ((~P and ~Q) or S) = (~P or S) and (~Q or S).
Step 4: Combine all resulting clauses:
CNF = (~P or R) and (~Q or R) and (~P or S) and (~Q or S).
Conclusion: CNF consists of 4 binary clauses.
Primary Academic References & Exam Sources
Every concept in Notes From a B.Tech Brain is synthesized from authoritative academic texts, seminal peer-reviewed research, verified exam archives, and renowned university lectures.