Chapter 4: Propositional Logic

4.1 Introduction to Propositional Logic¶

Propositional logic (also called Boolean logic or sentential logic) is the foundation of knowledge representation and automated reasoning in AI. It provides a formal language for expressing facts and a calculus for deriving new facts.

Why Logic in AI?¶

Advantages of Logic:

1. Declarative: Specify what is true, not how to compute it

2. Compositional: Build complex statements from simple ones using connectives

3. Unambiguous: Precise mathematical semantics

4. Inference: Automatically derive new knowledge from existing knowledge

5. Explainable: Reasoning steps are transparent and traceable

6. General: Apply same inference rules to any domain

Real-World Applications:

• Expert systems (medical diagnosis, financial advising)

• Hardware verification (chip design correctness)

• Software verification (program correctness proofs)

• Planning and scheduling systems

• Natural language understanding

• Semantic web and knowledge graphs

• Circuit design and optimization

• Database query optimization

4.2 Syntax of Propositional Logic¶

Atomic Propositions¶

Atomic propositions (or propositional symbols) are the basic building blocks:

• Denoted by capital letters: $P, Q, R, S, ...$

• Each represents a statement that is either true or false

• Examples:

  • $P$: “It is raining”

  • $Q$: “I have an umbrella”

  • $R$: “I will get wet”

Logical Connectives¶

We combine atomic propositions using logical connectives:

Well-Formed Formulas (WFF)¶

Definition: A formula is well-formed if constructed by these rules:

1. Every atomic proposition is a WFF

2. If $\alpha$ is a WFF, then $\neg \alpha$ is a WFF

3. If $\alpha$ and $\beta$ are WFFs, then:

   • $(\alpha \land \beta)$ is a WFF

   • $(\alpha \lor \beta)$ is a WFF

   • $(\alpha \rightarrow \beta)$ is a WFF

   • $(\alpha \leftrightarrow \beta)$ is a WFF

Examples:

• $P \land Q$ ✓

• $(P \rightarrow Q) \lor R$ ✓

• $\neg(P \land \neg Q)$ ✓

• $P \land \land Q$ ✗ (not well-formed)

4.3 Semantics: Meaning of Formulas¶

Truth Values¶

Every proposition has a truth value: true (T, 1) or false (F, 0).

Models¶

A model (or interpretation) is an assignment of truth values to all propositional symbols.

Example: For symbols $\{P, Q, R\}$, one model is:

Truth Tables for Connectives¶

Negation ($\neg$):

Conjunction ($\land$):

Disjunction ($\lor$):

Implication ($\rightarrow$):

Key insight: $P \rightarrow Q$ is equivalent to $\neg P \lor Q$

Biconditional ($\leftrightarrow$):

Key insight: $P \leftrightarrow Q$ means $(P \rightarrow Q) \land (Q \rightarrow P)$

4.4 Logical Equivalences¶

Two formulas $\alpha$ and $\beta$ are logically equivalent ($\alpha \equiv \beta$) if they have the same truth value in all models.

Important Equivalences¶

Identity Laws:

• $P \land \text{true} \equiv P$

• $P \lor \text{false} \equiv P$

Domination Laws:

• $P \land \text{false} \equiv \text{false}$

• $P \lor \text{true} \equiv \text{true}$

Idempotent Laws:

• $P \land P \equiv P$

• $P \lor P \equiv P$

Double Negation:

• $\neg(\neg P) \equiv P$

Commutative Laws:

• $P \land Q \equiv Q \land P$

• $P \lor Q \equiv Q \lor P$

Associative Laws:

• $(P \land Q) \land R \equiv P \land (Q \land R)$

• $(P \lor Q) \lor R \equiv P \lor (Q \lor R)$

Distributive Laws:

• $P \land (Q \lor R) \equiv (P \land Q) \lor (P \land R)$

• $P \lor (Q \land R) \equiv (P \lor Q) \land (P \lor R)$

De Morgan’s Laws:

• $\neg(P \land Q) \equiv \neg P \lor \neg Q$

• $\neg(P \lor Q) \equiv \neg P \land \neg Q$

Implication Elimination:

• $P \rightarrow Q \equiv \neg P \lor Q$

Biconditional Elimination:

• $P \leftrightarrow Q \equiv (P \rightarrow Q) \land (Q \rightarrow P)$

• $P \leftrightarrow Q \equiv (P \land Q) \lor (\neg P \land \neg Q)$

4.5 Satisfiability, Validity, and Entailment¶

Satisfiability¶

A formula is satisfiable if there exists at least one model where it is true.

Example: $P \land Q$ is satisfiable (true when $P=T, Q=T$)

A formula is unsatisfiable (contradiction) if it is false in all models.

Example: $P \land \neg P$ is unsatisfiable

Validity¶

A formula is valid (tautology) if it is true in all models.

Examples:

• $P \lor \neg P$ (Law of Excluded Middle)

• $\neg(P \land \neg P)$ (Law of Non-contradiction)

• $(P \rightarrow Q) \leftrightarrow (\neg Q \rightarrow \neg P)$ (Contrapositive)

Logical Entailment¶

A knowledge base $KB$ entails a formula $\alpha$ (written $KB \models \alpha$) if $\alpha$ is true in all models where $KB$ is true.

Example:

• $KB$: $P \rightarrow Q, P$

• Then $KB \models Q$ (by Modus Ponens)

Key Relationship:

This is the basis for refutation theorem proving.

4.6 Conjunctive Normal Form (CNF)¶

Definition¶

A formula is in Conjunctive Normal Form if it is a conjunction of clauses, where each clause is a disjunction of literals.

Literal: An atomic proposition or its negation ($P$ or $\neg P$)

Clause: Disjunction of literals ($L_1 \lor L_2 \lor ... \lor L_n$)

CNF: Conjunction of clauses $(C_1 \land C_2 \land ... \land C_m)$

Examples:

• $(P \lor Q) \land (\neg P \lor R)$ ✓ (in CNF)

• $(P \land Q) \lor R$ ✗ (not in CNF)

Conversion to CNF¶

Algorithm:

1. Eliminate implications and biconditionals:

   • $P \rightarrow Q \Rightarrow \neg P \lor Q$

   • $P \leftrightarrow Q \Rightarrow (\neg P \lor Q) \land (\neg Q \lor P)$

2. Move negation inward (De Morgan’s laws):

   • $\neg(P \land Q) \Rightarrow \neg P \lor \neg Q$

   • $\neg(P \lor Q) \Rightarrow \neg P \land \neg Q$

   • $\neg \neg P \Rightarrow P$

3. Distribute $\lor$ over $\land$:

   • $P \lor (Q \land R) \Rightarrow (P \lor Q) \land (P \lor R)$

Example Conversion:

Convert $\neg(P \rightarrow Q)$ to CNF:

1. Eliminate implication: $\neg(\neg P \lor Q)$

2. De Morgan: $\neg \neg P \land \neg Q$

3. Double negation: $P \land \neg Q$

Result: $(P) \land (\neg Q)$ (in CNF)

4.7 Model Checking¶

Model checking determines if $KB \models \alpha$ by enumerating all possible models.

Truth Table Enumeration¶

Algorithm: TT-ENTAILS?(KB, α)

begin
    symbols ← all propositional symbols in KB and α
    return TT-CHECK-ALL(KB, α, symbols, {})
end

Algorithm: TT-CHECK-ALL(KB, α, symbols, model)

begin
    if symbols is empty then
        if KB is true in model then
            return α is true in model
        else
            return true  // KB false, so entailment holds vacuously
    else
        P ← FIRST(symbols)
        rest ← REST(symbols)
        return TT-CHECK-ALL(KB, α, rest, model ∪ {P: true})
           and TT-CHECK-ALL(KB, α, rest, model ∪ {P: false})
end

Complexity: $O(2^n)$ where $n$ is the number of symbols

Sound: Yes - only returns true if entailment holds

Complete: Yes - always terminates with correct answer

4.8 Resolution Theorem Proving¶

Resolution is a single inference rule that is sound and refutation-complete for propositional logic.

Resolution Rule¶

From two clauses containing complementary literals, infer a new clause:

Example:

Resolution Algorithm¶

To prove $KB \models \alpha$, show that $(KB \land \neg \alpha)$ is unsatisfiable:

Algorithm: PL-RESOLUTION(KB, α)

begin
    clauses ← CNF(KB ∧ ¬α)
    new ← {}
    
    loop
        for each pair (Ci, Cj) of clauses in clauses do
            resolvents ← PL-RESOLVE(Ci, Cj)
            
            if resolvents contains empty clause then
                return true  // Proved by contradiction
            
            new ← new ∪ resolvents
        
        if new ⊆ clauses then
            return false  // No new clauses, cannot prove
        
        clauses ← clauses ∪ new
end

Algorithm: PL-RESOLVE(Ci, Cj)

begin
    resolvents ← {}
    
    for each literal ℓ in Ci do
        if ¬ℓ in Cj then
            resolvent ← (Ci - {ℓ}) ∪ (Cj - {¬ℓ})
            resolvents ← resolvents ∪ {resolvent}
    
    return resolvents
end

Properties:

• Sound: Only derives true conclusions

• Refutation-complete: Can prove all entailments by contradiction

• Complexity: Exponential in worst case

Resolution Example¶

Prove: $KB \models R$ where $KB = \{P \rightarrow Q, Q \rightarrow R, P\}$

1. Convert to CNF:

   • $\neg P \lor Q$

   • $\neg Q \lor R$

   • $P$

   • $\neg R$ (negated query)

2. Apply resolution:

   • Resolve $P$ and $\neg P \lor Q$: get $Q$

   • Resolve $Q$ and $\neg Q \lor R$: get $R$

   • Resolve $R$ and $\neg R$: get empty clause $\square$

3. Empty clause derived → proved!

4.9 DPLL Algorithm for SAT¶

The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is an efficient method for determining satisfiability.

Key Ideas¶

1. Early termination: Stop as soon as formula is satisfied or unsatisfied

2. Pure symbol heuristic: If symbol appears only positive or only negative, assign accordingly

3. Unit clause heuristic: If clause has only one literal, that literal must be true

4. Backtracking search: Try assignments systematically

DPLL Algorithm¶

Algorithm: DPLL(clauses, symbols, model)

begin
    if every clause in clauses is true in model then
        return true
    
    if some clause in clauses is false in model then
        return false
    
    // Pure symbol heuristic
    P, value ← FIND-PURE-SYMBOL(symbols, clauses, model)
    if P is non-null then
        return DPLL(clauses, symbols - P, model ∪ {P: value})
    
    // Unit clause heuristic
    P, value ← FIND-UNIT-CLAUSE(clauses, model)
    if P is non-null then
        return DPLL(clauses, symbols - P, model ∪ {P: value})
    
    // Splitting: try both values
    P ← FIRST(symbols)
    rest ← REST(symbols)
    
    return DPLL(clauses, rest, model ∪ {P: true})
        or DPLL(clauses, rest, model ∪ {P: false})
end

Improvements over basic search:

• Much faster in practice

• Still exponential worst-case

• Foundation of modern SAT solvers

4.10 Horn Clauses and Forward/Backward Chaining¶

Horn Clauses¶

A Horn clause is a clause with at most one positive literal.

Forms:

1. Definite clause: Exactly one positive literal

   • Example: $\neg P \lor \neg Q \lor R$ (equivalent to $P \land Q \rightarrow R$)

2. Fact: Single positive literal

   • Example: $P$

3. Goal clause: No positive literals

   • Example: $\neg P \lor \neg Q$ (equivalent to $\neg(P \land Q)$)

Why Horn clauses?

• Many real-world KBs naturally expressed as Horn clauses

• Inference is linear time in size of KB

• Foundation of logic programming (Prolog)

Forward Chaining¶

Forward chaining is data-driven inference: start with facts, apply rules to derive new facts.

Algorithm: FORWARD-CHAIN(KB, query)

begin
    count ← table of number of premises for each rule
    inferred ← table, initially all false
    agenda ← queue of facts, initially all facts in KB
    
    while agenda is not empty do
        p ← POP(agenda)
        
        if p = query then
            return true
        
        if inferred[p] = false then
            inferred[p] ← true
            
            for each rule (premises → conclusion) where p is in premises do
                count[rule] ← count[rule] - 1
                
                if count[rule] = 0 then
                    ADD conclusion to agenda
    
    return false
end

Properties:

• Complete: For definite clauses

• Time: $O(pn)$ where $p$ = number of rules, $n$ = number of symbols

• Space: Linear in KB size

• Monotonic: Inferred facts never retracted

Backward Chaining¶

Backward chaining is goal-driven inference: start with query, work backward to find supporting facts.

Algorithm: BACKWARD-CHAIN(KB, query)

begin
    if query is a known fact in KB then
        return true
    
    for each rule (premises → conclusion) where conclusion = query do
        if BACKWARD-CHAIN-ALL(KB, premises) then
            return true
    
    return false
end

Algorithm: BACKWARD-CHAIN-ALL(KB, premises)

begin
    for each premise in premises do
        if not BACKWARD-CHAIN(KB, premise) then
            return false
    
    return true
end

Properties:

• Complete: For definite clauses

• Efficient: Only explores relevant parts of KB

• Depth-first: Can get stuck in infinite loops (need loop detection)

Forward vs. Backward Chaining¶

4.11 Summary¶

Key Concepts¶

1. Syntax: Propositions and connectives

2. Semantics: Truth values and models

3. CNF: Standard form for inference

4. Entailment: Logical consequence

5. Model checking: Truth table enumeration

6. Resolution: Refutation-complete inference

7. DPLL: Efficient SAT solving

8. Horn clauses: Restricted but tractable

9. Forward/Backward chaining: Efficient for Horn clauses

Inference Methods Comparison¶

*Refutation-complete, **For Horn clauses

Limitations of Propositional Logic¶

1. Cannot express:

   • Quantification (all, some)

   • Objects and relations

   • Functions

2. Lack of abstraction: Must enumerate all instances

3. Solution: First-Order Logic (Chapter 5)

4.12 Implementation¶

For complete Python implementations, see:

Chapter 4: Propositional Logic - Implementation

The implementation notebook includes:

1. Expression Classes: Symbol, Not, And, Or, Implies, Biconditional

2. Truth Table Generation: Enumerate all models

3. CNF Conversion: Transform any formula to CNF

4. Resolution Prover: Theorem proving by refutation

5. DPLL SAT Solver: Efficient satisfiability checking

6. Forward Chaining: Data-driven inference for Horn clauses

7. Backward Chaining: Goal-driven inference

8. Knowledge Base: Store and query facts and rules

9. Real-World Applications:

   • Logic puzzle solver (Einstein’s riddle)

   • Sudoku as SAT problem

   • Expert system for classification

Further Reading¶

Textbooks¶

• Aggarwal, C. C. (2021). Artificial Intelligence: A Textbook. Springer. [Chapter 4]

• Russell, S., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th ed.). Pearson. [Chapter 7]

• Genesereth, M., & Nilsson, N. (1987). Logical Foundations of Artificial Intelligence. Morgan Kaufmann.

Classic Papers¶

• Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM.

• Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM.

• Cook, S. A. (1971). The complexity of theorem-proving procedures. STOC.

Modern SAT Solvers¶

• Biere, A., et al. (2009). Handbook of Satisfiability. IOS Press.

• Marques-Silva, J., & Sakallah, K. A. (1999). GRASP: A search algorithm for propositional satisfiability. IEEE TC.

Online Resources¶

• SAT Competition

• Logic in Computer Science

• Automated Theorem Proving