CNF Conversion, Skolemization, Unification & Resolution
“Converting to clausal form, Most General Unifier (MGU), and proving theorems via contradiction.”
1.First-Order Logic (FOL) Formalism & Clausal Form Conversion
§ 4.1.First-Order Logic extends propositional logic by introducing objects, relations (predicates), functions, and quantifiers (\forall universal, \exists existential).
The 6-Step Clausal Form (CNF) Pipeline:
1. Eliminate Implications: Replace P \implies Q with \neg P \lor Q, and P \iff Q with (\neg P \lor Q) \land (\neg Q \lor P).
2. Move Negations Inward: \neg \forall x P(x) \equiv \exists x \neg P(x); \neg \exists x P(x) \equiv \forall x \neg P(x).
3. Standardize Variables: Ensure each quantifier uses a distinct variable name: (\forall x P(x)) \lor (\forall x Q(x)) \implies (\forall x P(x)) \lor (\forall y Q(y)).
4. Skolemization (Eliminate \exists):
• Outside scope of any \forall: Replace \exists x P(x) with P(A), where A is a new Skolem Constant.
• Inside scope of \forall x_1, ..., x_k: Replace \exists y P(y) with P(f(x_1, ..., x_k)), where f is a new Skolem Function.
5. Drop Universal Quantifiers: All remaining variables are implicitly universally quantified.
6. Distribute \lor over \land: Produce a conjunction of clauses (each clause is a disjunction of literals).
2.The Unification Algorithm & Most General Unifier (MGU)
§ 4.2.To resolve two complementary literals with different variable names (e.g. P(x) and \neg P(John)), inference engines execute Unification.
Definition (MGU):
A substitution \theta = {v_1 / t_1, v_2 / t_2, ...} is a unifier for literals p and q if Subst(\theta, p) = Subst(\theta, q). An MGU is the unique (up to variable renaming) most general unifier that makes the least commitment to variable bindings.
The Occurs-Check Rule:
A variable x cannot unify with a term t if x occurs inside t (e.g. cannot unify x with f(x)). Attempting to do so creates an infinite cyclic term f(f(f(...))).
3. GATE DA Worked Example: Most General Unifier (MGU)
Apply substitutions from earlier arguments to subsequent arguments before matching them!
Problem (Original Practice Problem · Modeled on GATE DA Pattern):
Find the Most General Unifier (MGU) theta for literals:
Literal 1: P(x, f(y), z)
Literal 2: P(a, f(g(w)), g(x))
(where a is a constant, and x, y, z, w are variables).
Step 1: Match 1st arguments: x and a.
Variable x unifies with constant a.
Substitution theta1 = { x / a }.
Step 2: Apply theta1 to remaining arguments of both literals:
Literal 1 becomes: P(a, f(y), z)
Literal 2 becomes: P(a, f(g(w)), g(a)) (notice x replaced by a).
Step 3: Match 2nd arguments: f(y) and f(g(w)):
Function symbols match (f == f).
Unify internal arguments: y and g(w).
Substitution theta2 = { y / g(w) }.
Step 4: Match 3rd arguments: z and g(a):
Variable z unifies with compound term g(a).
Substitution theta3 = { z / g(a) }.
Step 5: Compose all substitutions:
MGU theta = { x / a, y / g(w), z / g(a) }.
Conclusion: MGU is { x / a, y / g(w), z / g(a) }.
4. GATE DA Worked Example: Resolution Refutation Theorem Proof
To prove theorem alpha, add NEGATION ~alpha to the Knowledge Base, NOT alpha itself!
Problem (Original Practice Problem · Modeled on GATE DA Pattern):
Given Knowledge Base KB in Clausal Form:
Clause 1: ~P(x) or Q(x)
Clause 2: P(A)
Clause 3: ~Q(y) or R(y)
Prove by Resolution Refutation that KB entails R(A).
Step 1: Negate the goal theorem:
Goal is R(A). Negated goal: ~R(A) (Clause 4).
Step 2: Resolve Clause 1 with Clause 2:
C1: ~P(x) or Q(x)
C2: P(A)
Unify P(x) with P(A) => theta = { x / A }.
Resolvent C5: Q(A).
Step 3: Resolve Clause 5 with Clause 3:
C5: Q(A)
C3: ~Q(y) or R(y)
Unify Q(y) with Q(A) => theta = { y / A }.
Resolvent C6: R(A).
Step 4: Resolve Clause 6 with Clause 4 (Negated Goal):
C6: R(A)
C4: ~R(A)
Resolvent C7: [] (Empty Clause / Contradiction).
Conclusion: Derivation of the Empty Clause proves that KB entails R(A) with mathematical certainty.
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.