Propositional Equivalences, Normal Forms & Inference Rules
“Tautologies, DNF/CNF canonical expansions, inference rules, and resolution refutation.”
1.Propositional Connectives & The Implication Axiom
§ 1.1.A Proposition is a declarative statement that is either TRUE or FALSE, but not both.
The Conditional Implication (p -> q):
The statement p -> q asserts that if hypothesis p holds, conclusion q must hold. It is FALSE in only one case: when p is TRUE and q is FALSE.
If p is FALSE, p -> q is vacuously TRUE regardless of q.
Canonical Equivalence Laws:
1. p -> q <=> neg p lor q (Implication Law)
2. p -> q <=> neg q -> neg p (Contrapositive Law)
3. neg(p -> q) <=> p land neg q
4. p <-> q <=> (p -> q) land (q -> p) <=> (p land q) lor (neg p land neg q)
Formulas Classification:
- Tautology: TRUE under all truth assignments.
- Contradiction: FALSE under all truth assignments.
- Contingency: Neither a tautology nor a contradiction.
- Satisfiable: TRUE under at least one assignment.
2.Canonical Normal Forms & Resolution Refutation
§ 1.2.Every boolean formula can be converted into standard normal forms:
1. Disjunctive Normal Form (DNF): OR of ANDs (Sum of Products).
2. Conjunctive Normal Form (CNF): AND of ORs (Product of Sums).
The Resolution Principle (Robinson):
Resolution is an inference rule that operates on clauses in CNF:
frac{(A lor B) quad land quad (neg B lor C)}{A lor C}
Here B and neg B are complementary literals that cancel out to produce the resolvent A lor C.
To prove that premise set Delta entails conclusion alpha (Delta models alpha):
Convert Delta cup {neg alpha} into CNF clauses and apply resolution. If the empty clause square (a contradiction) is derived, alpha is valid.
3. Worked Problem: Testing Argument Validity via Resolution
To prove validity by refutation, you must negate the conclusion before resolving.
Problem: Determine the validity of the argument with premises P1: p -> (q v r), P2: ~q, P3: ~r, and conclusion C: ~p.
Step 1: Convert premises and negated conclusion into CNF clauses:
P1: p -> (q v r) <=> ~p v q v r (Clause 1: {~p, q, r})
P2: ~q (Clause 2: {~q})
P3: ~r (Clause 3: {~r})
Negated Conclusion ~C: ~(~p) <=> p (Clause 4: {p})
Step 2: Apply resolution steps:
- Resolve Clause 1 {~p, q, r} with Clause 4 {p}:
Complementary literals p and ~p cancel => Resolvent R1: {q, r}.
- Resolve R1 {q, r} with Clause 2 {~q}:
Complementary literals q and ~q cancel => Resolvent R2: {r}.
- Resolve R2 {r} with Clause 3 {~r}:
Complementary literals r and ~r cancel => Resolvent R3: {} (Empty Clause / Contradiction).
Step 3: Conclusion:
Derivation of the empty clause confirms that P1 ^ P2 ^ P3 ^ p is unsatisfiable.
Therefore, the original argument is VALID.
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.
Curated for clarity, rigorous numerical solving, and semester excellence:
GATE-focused discrete maths with formula-sheet style rapid coverage.
All relation/function counting formulas in exam-pattern format.
University-level rigour with engaging visual proofs.