Skip to main content
⚡ Calmops
🤖 AI 🏗️ Architecture 🌐 Web 🗃️ Database ⚙️ DevOps 🌍 Network 💻 Programming 🧮 Algorithms 📐 Software Eng. ☁️ Cloud 🔒 Security 📈 Finance More →

From First-Order Logic to Clausal Form: A Step-by-Step Guide

Created: February 20, 2026 CalmOps 6 min read

From First-Order Logic to Clausal Form: A Step-by-Step Guide

TL;DR: Converting first-order logic (FOL) formulas to clausal form is essential for resolution-based theorem proving. This guide walks through the complete 8-step transformation process with a detailed worked example.

Introduction

In first-order logic, we work with formulas containing quantifiers (∀ for “for all”, ∃ for “exists”), predicates, variables, and logical connectives. While FOL provides expressive power for representing knowledge, automated reasoning algorithms like resolution require formulas in a specific standardized format: clausal form (also called clause normal form).

Clausal form represents formulas as a set of clauses, where each clause is a disjunction of literals. This standardized format enables efficient automated theorem proving and serves as the foundation for logic programming languages like Prolog.

The transformation from an arbitrary FOL formula to clausal form follows a systematic 8-step procedure. Let’s explore each step in detail.

The 8-Step Transformation Process

Step 1: Eliminate Implications and Biconditionals

The first step removes the → (implication) and ↔ (biconditional) connectives, rewriting them using only ¬, ∧, and ∨.

Transformation rules:

  • Implication elimination: P → Q becomes ¬P ∨ Q
  • Biconditional elimination: P ↔ Q becomes (P → Q) ∧ (Q → Q) which expands to (¬P ∨ Q) ∧ (¬Q ∨ P)

This simplification ensures that negations only apply to atomic formulas, making subsequent transformations more straightforward.

Step 2: Move Negations Inward (Negation Normal Form)

This step applies De Morgan’s laws and quantifier negations to push ¬ operators inside the formula until they appear only before atomic predicates.

Key transformation rules:

  • ¬(P ∧ Q) becomes ¬P ∨ ¬Q
  • ¬(P ∨ Q) becomes ¬P ∧ ¬Q
  • ¬∀x P becomes ∃x ¬P
  • ¬∃x P becomes ∀x ¬P
  • ¬¬P becomes P (double negation elimination)

The result is a formula in negation normal form (NNF) where negations appear only before atomic formulas.

Step 3: Standardize Variables Apart

When quantifiers appear multiple times in a formula, variables with the same name can cause conflicts. This step renames variables to ensure each quantifier binds a unique variable name.

For example, in ∀x P(x) ∧ ∃x Q(x), we rename to ∀x P(x) ∧ ∃y Q(y).

This step prevents unintended variable capture during Skolemization and ensures correct scope handling.

Step 4: Eliminate Existential Quantifiers (Skolemization)

Skolemization removes existential quantifiers by introducing Skolem functions or Skolem constants.

  • If ∃x P(x) falls within the scope of universal quantifiers ∀y₁, ∀y₂, ..., replace x with a Skolem function f(y₁, y₂, ...)
  • If ∃x has no enclosing universal quantifiers, replace x with a Skolem constant (a function of zero arguments)

Example:

  • ∀x ∃y Loves(x, y) becomes ∀x Loves(x, f(x)) where f is a Skolem function

Skolemization preserves satisfiability: the original formula is satisfiable if and only if the Skolemized formula is satisfiable.

Step 5: Drop Universal Quantifiers

After Skolemization, all remaining quantifiers are universal. Since clauses implicitly have universal quantification in clausal form, we can drop all ∀ quantifiers.

For example, ∀x ∀y P(x, y) becomes simply P(x, y).

Step 6: Convert to Conjunctive Normal Form (CNF)

A formula is in CNF if it is a conjunction of disjunctions: (A₁ ∨ A₂ ∨ ...) ∧ (B₁ ∨ B₂ ∨ ...) ∧ ...

This step applies the distributive law:

  • P ∨ (Q ∧ R) becomes (P ∨ Q) ∧ (P ∨ R)

We restructure the formula so all ∧ operators are outside all ∨ operators.

Step 7: Distribute Disjunctions Over Conjunctions

This is actually part of the CNF conversion. We ensure that:

  • No disjunction appears within a conjunction’s scope in a way that would prevent CNF structure
  • The formula becomes a flat conjunction of disjunctions

Step 8: Separate into Individual Clauses

The final step extracts each conjunct as a separate clause. Each clause is a set of literals (disjunction), and the entire formula becomes a set of clauses.

This is the format required for resolution: we reason about individual clauses rather than the complete formula.

Worked Example

Let’s transform the following FOL formula through all steps:

Original Formula:

∀x [P(x) → (∃y [Q(y) ∧ R(x, y)])]

Step 1: Eliminate Implications

∀x [¬P(x) ∨ (∃y [Q(y) ∧ R(x, y)])]

Step 2: Move Negations Inward

The negation is already applied only to atomic formulas. The ∃y is already in the correct position:

∀x [¬P(x) ∨ (∃y [Q(y) ∧ R(x, y)])]

Step 3: Standardize Variables Apart

We have only one universal quantifier ∀x and one existential ∃y. Since they differ, no renaming needed here. However, let’s verify scope:

∀x [¬P(x) ∨ (∃y [Q(y) ∧ R(x, y)])]

Step 4: Skolemization

The existential quantifier ∃y is within the scope of ∀x. We introduce a Skolem function f(x):

∀x [¬P(x) ∨ (Q(f(x)) ∧ R(x, f(x)))]

Step 5: Drop Universal Quantifiers

¬P(x) ∨ (Q(f(x)) ∧ R(x, f(x)))

Step 6: Convert to CNF

Apply distribution: A ∨ (B ∧ C) becomes (A ∨ B) ∧ (A ∨ C)

(¬P(x) ∨ Q(f(x))) ∧ (¬P(x) ∨ R(x, f(x)))

Step 7: Distribute Disjunctions

Already done in Step 6. The formula is now in CNF.

Step 8: Separate into Clauses

Clause 1: ¬P(x) ∨ Q(f(x))
Clause 2: ¬P(x) ∨ R(x, f(x))

Another Worked Example

Let’s try a more complex formula:

Original Formula:

¬∀x [P(x) → ∃y Q(x, y)]

Step 1: Eliminate Implications

First, rewrite implication:

¬∀x [¬P(x) ∨ ∃y Q(x, y)]

Step 2: Move Negations Inward

Apply negation to universal quantifier and De Morgan’s laws:

∃x ¬[¬P(x) ∨ ∃y Q(x, y)]
∃x [¬(¬P(x) ∨ ∃y Q(x, y))]
∃x [¬¬P(x) ∧ ¬∃y Q(x, y)]
∃x [P(x) ∧ ∀y ¬Q(x, y)]

Step 3: Standardize Variables Apart

∃x [P(x) ∧ ∀y ¬Q(x, y)]

Step 4: Skolemization

The existential quantifier ∃x has no enclosing universal quantifiers, so we introduce a Skolem constant a:

P(a) ∧ ∀y ¬Q(a, y)

Step 5: Drop Universal Quantifiers

P(a) ∧ ¬Q(a, y)

Step 6 & 7: CNF Conversion

The formula is already in CNF (conjunction of two literals).

Step 8: Separate into Clauses

Clause 1: P(a)
Clause 2: ¬Q(a, y)

Why This Matters

The clausal form transformation is fundamental to:

  1. Resolution-based theorem proving: Resolution operates on clauses, combining them to derive new clauses until a contradiction (empty clause) is found.

  2. Logic programming: Prolog programs are essentially sets of clauses in a specific form called Horn clauses.

  3. Knowledge representation: Many knowledge representation formalisms convert to clausal form for reasoning.

  4. SAT solving: While SAT solvers typically work with propositional CNF, the same principles apply.

Common Pitfalls and Tips

Pitfall Solution
Forgetting to Skolemize before dropping quantifiers Always Skolemize first, then drop universal quantifiers
Incorrect variable renaming Use fresh variable names for each quantifier scope
Applying distribution incorrectly Remember: A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)

Conclusion

The systematic 8-step process transforms any first-order logic formula into clausal form. While each step has well-defined rules, the process requires careful attention to variable scoping and quantifier interactions. Mastery of this transformation is essential for working with automated theorem provers, SAT solvers, and logic programming systems.

In practice, these transformations are automated by software tools. However, understanding the underlying process helps debugging, formal verification, and when implementing reasoning systems from scratch.

References

  • Robinson, J. A. (1965). “A Machine-Oriented Logic Based on the Resolution Principle”
  • Chang, C. L., & Lee, R. C. T. (1973). “Symbolic Logic and Mechanical Theorem Proving”
  • Fitting, M. (1996). “First-Order Logic and Automated Theorem Proving”

Comments