Propositional Logic

Logical Foundation for Knowledge Representation and Reasoning

Introduction

Propositional logic formal system for reasoning about propositions (statements with truth values). Allows representing knowledge using logical formulas, deriving new facts via inference rules. Foundation for knowledge-based systems, automated reasoning, theorem proving.

Simple but powerful: any knowledge expressible as propositions can be represented. Trade-off: limited expressiveness (can't quantify, relate properties). First-order logic extends with predicates and quantifiers (later topic).

Core task: given knowledge base (set of formulas), determine if new formula logically follows (entailment). Key insight: entailment reducible to satisfiability (formula unsatisfiable iff negation entailed).

"Propositional logic is the simplest formal system for reasoning. While limited, it's complete and sound foundation for more complex logical systems." -- Mathematical logic foundations

Propositions and Truth Values

Definition

Proposition: statement declaring fact, has truth value true or false (not both, not neither). Examples: "It is raining", "2 + 2 = 4", "Paris is capital of France".

Propositional Variables

Use symbols (P, Q, R, ...) representing propositions. P might represent "It is raining". Without specific interpretation, P has unknown truth value (true in some worlds, false in others).

Interpretation (Model)

Assignment of truth values to all propositional variables. Example: P=true, Q=false, R=true. Different interpretations → different truth values for formulas.

Atomic Formulas

Single propositional variable (P, Q, R). Building blocks. Combined using connectives to form complex formulas.

Logical Connectives

Negation (NOT) ¬

¬P true when P false, false when P true. Example: ¬(It is raining) = It is not raining.

Conjunction (AND) ∧

P ∧ Q true only when both P and Q true. "It is raining AND it is cold".

Disjunction (OR) ∨

P ∨ Q true when at least one of P or Q true. Inclusive OR (true if both also).

Implication (IMPLIES) →

P → Q false only when P true and Q false. "If it rains, then ground wet". Equivalent to ¬P ∨ Q.

Biconditional (IFF) ↔

P ↔ Q true when P and Q have same truth value. "It rains IFF ground wet".

Truth table summary:
P | Q | ¬P | P∧Q | P∨Q | P→Q | P↔Q
T | T | F | T | T | T | T
T | F | F | F | T | F | F
F | T | T | F | T | T | F
F | F | T | F | F | T | T

Truth Tables and Semantics

Computing Formula Truth Values

Build truth table for formula: list all possible interpretations, compute formula value under each.

Example: (P ∨ Q) → ¬(P ∧ Q)

P | Q | P∨Q | P∧Q | ¬(P∧Q) | (P∨Q)→¬(P∧Q)
T | T | T | T | F | F
T | F | T | F | T | T
F | T | T | F | T | T
F | F | F | F | T | T

Formula true in 3 out of 4 interpretations (satisfiable but not tautology)

Tautology, Contingency, Contradiction

  • Tautology: true in all interpretations (P ∨ ¬P)
  • Contingency: true in some, false in others
  • Contradiction: false in all interpretations (P ∧ ¬P)

Number of Interpretations

n propositional variables → 2^n interpretations. For n=10, 1024 interpretations. For n=20, 1 million. Truth tables exponential in variables.

Well-Formed Formulas (WFF)

Syntax Rules

Well-formed formulas defined recursively: (1) propositional variable is WFF, (2) if F is WFF, so is ¬F, (3) if F and G are WFF, so are (F∧G), (F∨G), (F→G), (F↔G).

Operator Precedence

Avoid ambiguity: ¬ highest, then ∧, then ∨, then →, then ↔. Example: P → Q ∧ ¬R means P → (Q ∧ (¬R)).

Parentheses

Use liberally for clarity. ((P ∧ Q) → (R ∨ ¬S)) unambiguous.

Logical Equivalence and Normal Forms

Equivalence

Formulas F and G logically equivalent if same truth value in all interpretations. Notation: F ≡ G.

De Morgan's Laws

¬(P ∧ Q) ≡ ¬P ∨ ¬Q
¬(P ∨ Q) ≡ ¬P ∧ ¬Q

Normal Forms

Conjunctive Normal Form (CNF): conjunction of disjunctions. (P ∨ Q) ∧ (¬R ∨ S). Every formula convertible to CNF.

Disjunctive Normal Form (DNF): disjunction of conjunctions. (P ∧ Q) ∨ (¬R ∧ S). Every formula convertible to DNF.

Conversion to CNF

1. Eliminate → : P → Q ≡ ¬P ∨ Q
2. Eliminate ↔ : P ↔ Q ≡ (¬P ∨ Q) ∧ (P ∨ ¬Q)
3. Apply De Morgan to push ¬ inside
4. Distribute ∨ over ∧ : P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R)

CNF Importance

Resolution (inference rule) works on CNF. Critical for automated reasoning.

Inference Rules and Proofs

Modus Ponens

P
P → Q
------
Q

If P true and P implies Q, then Q true.

Modus Tollens

¬Q
P → Q
------
¬P

If Q false and P implies Q, then P false.

Disjunctive Syllogism

P ∨ Q
¬P
------
Q

If P or Q, and P false, then Q true.

Proof

Sequence of formulas, each following from previous by inference rule. If can derive Q from knowledge base KB, then KB ⊢ Q (Q provable from KB).

Soundness and Completeness

Inference rules sound: if KB ⊢ Q then KB ⊨ Q (what provable is true). Complete: if KB ⊨ Q then KB ⊢ Q (what true is provable).

Resolution Principle

Resolution Rule

P ∨ A
¬P ∨ B
-------
A ∨ B

Resolvent: simplified disjunction dropping complementary literals P and ¬P.

Proof by Contradiction (Resolution Refutation)

To prove KB ⊢ Q: assume ¬Q, convert KB ∪ {¬Q} to CNF, apply resolution until derive empty clause (contradiction). If contradiction derived, Q provable.

Algorithm

1. Convert KB ∪ {¬Q} to CNF (set of clauses)
2. While contradiction not found:
 - Select two clauses with complementary literals
 - Apply resolution, add resolvent to set
 - If empty clause derived: return TRUE (Q provable)
 - If no new clauses: return FALSE (Q not provable)

Advantage

Resolution complete: can prove all entailed formulas. Single rule sufficient (unlike multiple inference rules needed).

Complexity

Resolution may require exponential steps (worst case 2^n clauses). NP-complete problem underlying.

Satisfiability and SAT Problem

SAT Problem

Given formula F, is there interpretation making F true? SAT hard (NP-complete). Many heuristics but no known efficient algorithm.

Relationship to Entailment

KB ⊨ Q iff KB ∧ ¬Q unsatisfiable. Check entailment by checking unsatisfiability of negation. Dual problems.

SAT Solvers

DPLL algorithm: depth-first search with backtracking, unit propagation, pure literal elimination. Modern solvers (CDCL) add conflict analysis, learning.

Applications

  • Circuit verification: circuit correct iff formula satisfiable
  • Scheduling: encode constraints as formula, SAT solver finds schedule
  • Planning: encode plan existence as SAT problem

Computational Complexity

NP-Completeness

SAT is NP-complete: verifying solution fast (polynomial), but finding solution hard (no known polynomial algorithm). Every NP problem reducible to SAT.

Practical Implications

No efficient algorithm known for SAT. But SAT solvers work well in practice (many benchmarks solvable). Theory vs. practice gap.

Computational Limits

Propositional inference tractable only for small knowledge bases. Real-world reasoning requires more efficient representations (first-order logic, description logics).

Applications in AI

Knowledge Representation

Encode knowledge as logical formulas. Query: does KB entail fact Q? Foundation for knowledge-based systems.

Planning

Plan exists iff formula representing plan constraints satisfiable. SAT-based planners competitive with classical planners.

Configuration and Diagnosis

Diagnose system failures: encode symptom-disease relationships, ask SAT solver what disease explains symptoms.

Ontology and Description Logic

Description logics (subsets of first-order logic) reducible to propositional logic via compilation. Enable efficient reasoning over ontologies.

Limitations and Extensions

Lack of Quantifiers

Can't express "all" or "some". First-order logic adds ∀ (for all) and ∃ (exists) quantifiers, enabling richer expressiveness.

No Relations

Can't relate objects: parent(john, mary). Must use propositions: john_parent_of_mary. Impractical for many domains.

Monotonicity

Once fact added to KB, always believed (monotonic). Realistic reasoning requires revising beliefs (non-monotonic). Extensions: default logic, circumscription.

Uncertainty

Propositional logic binary (true/false). Real-world reasoning involves uncertainty: Bayesian networks, fuzzy logic handle probability/degrees of truth.

First-Order Logic

More expressive than propositional (predicates, quantifiers). But inference harder (semi-decidable, no complete efficient algorithm). Practical systems use restricted fragments.

References

  • Russell, S. J., and Norvig, P. "Artificial Intelligence: A Modern Approach." Prentice Hall, 4th edition, 2020.
  • Mendelson, E. "Introduction to Mathematical Logic." Chapman & Hall, 6th edition, 2015.
  • Huth, M., and Ryan, M. "Logic in Computer Science." Cambridge University Press, 2nd edition, 2004.
  • Van Dalen, D. "Logic and Structure." Springer, 5th edition, 2013.
  • Fitting, M. "First-Order Logic and Automated Theorem Proving." Springer, 2nd edition, 1996.