5.3 Prenex, Skolem, and clausal normal forms

Normal forms in first-order logic help simplify complex formulas. Prenex normal form moves quantifiers to the front, Skolem normal form eliminates existential quantifiers, and clausal normal form breaks formulas into conjunctions of disjunctions.

These transformations are crucial for automated reasoning and theorem proving. By converting formulas to these standard forms, we can apply efficient algorithms for logical inference and manipulation, making complex logical problems more manageable.

Normal Forms of First-Order Logic

Definition of Prenex Normal Form

Top images from around the web for Definition of Prenex Normal Form

• 

  Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via ... View original

  Is this image relevant?

• 

  Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via ... View original

  Is this image relevant?

1 of 1

Top images from around the web for Definition of Prenex Normal Form

• 

  Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via ... View original

  Is this image relevant?

• 

  Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via ... View original

  Is this image relevant?

1 of 1

• Prenex normal form is a first-order logic formula where all quantifiers appear at the beginning of the formula, followed by a quantifier-free matrix
• The quantifiers are grouped together and moved to the front of the formula, while the remaining formula (matrix) contains no quantifiers
• Example: $\forall x \exists y (P(x) \rightarrow Q(y))$ is in prenex normal form

Definition of Skolem Normal Form

• Skolem normal form is a formula in prenex normal form where all existential quantifiers have been eliminated by replacing existentially quantified variables with Skolem functions or Skolem constants
• Existentially quantified variables are replaced with functions (Skolem functions) that depend on the universally quantified variables preceding them
• If no universally quantified variables precede an existentially quantified variable, it is replaced with a constant (Skolem constant)
• Example: $\forall x \forall y (P(x, f(x, y)) \rightarrow Q(y))$ is in Skolem normal form, where $f$ is a Skolem function

Definition of Clausal Normal Form

• Clausal normal form, also known as conjunctive normal form, is a formula in Skolem normal form that consists of a conjunction of clauses, where each clause is a disjunction of literals
  • A literal is an atomic formula or the negation of an atomic formula
  • In clausal normal form, the conjunction of clauses is often represented as a set of clauses, and each clause is represented as a set of literals
• The formula is a conjunction (AND) of clauses, and each clause is a disjunction (OR) of literals
• Example: $\{\{P(a), \neg Q(b)\}, \{\neg P(c), R(d)\}\}$ is in clausal normal form, representing the formula $(P(a) \vee \neg Q(b)) \wedge (\neg P(c) \vee R(d))$

Conversion to Prenex Normal Form

Moving Quantifiers to the Beginning of the Formula

• To convert a formula into prenex normal form, move all quantifiers to the beginning of the formula while preserving the formula's logical equivalence
• Use the following equivalence rules to move quantifiers:
  • $(\forall x A) \wedge B \equiv \forall x (A \wedge B)$, if $x$ does not occur free in $B$
  • $(\exists x A) \wedge B \equiv \exists x (A \wedge B)$, if $x$ does not occur free in $B$
  • $(\forall x A) \vee B \equiv \forall x (A \vee B)$, if $x$ does not occur free in $B$
  • $(\exists x A) \vee B \equiv \exists x (A \vee B)$, if $x$ does not occur free in $B$
• Example: $\forall x P(x) \wedge \exists y Q(y)$ can be converted to $\forall x \exists y (P(x) \wedge Q(y))$

Renaming Variables and Obtaining the Matrix

• Rename variables as necessary to avoid variable capture when moving quantifiers
  • Variable capture occurs when a variable becomes bound by a quantifier it was not originally bound by
• After moving all quantifiers to the beginning of the formula, the remaining formula is called the matrix, which should be quantifier-free
• Example: $\forall x \exists y (P(x) \wedge \forall y Q(y))$ should be renamed to $\forall x \exists y (P(x) \wedge \forall z Q(z))$ to avoid variable capture, with the matrix being $P(x) \wedge \forall z Q(z)$

Transformation to Skolem Normal Form

Eliminating Existential Quantifiers

• To convert a formula in prenex normal form into Skolem normal form, eliminate all existential quantifiers by replacing existentially quantified variables with Skolem functions or Skolem constants
• For each existentially quantified variable, introduce a new function symbol (Skolem function) that depends on the universally quantified variables preceding the existential quantifier
  • If there are no universally quantified variables preceding the existential quantifier, replace the existentially quantified variable with a new constant symbol (Skolem constant)
• Example: $\forall x \exists y P(x, y)$ can be converted to $\forall x P(x, f(x))$, where $f$ is a Skolem function

Removing Existential Quantifiers and Obtaining Skolem Normal Form

• After replacing all existentially quantified variables with Skolem functions or constants, remove the existential quantifiers from the formula
• The resulting formula is in Skolem normal form, containing only universal quantifiers followed by a quantifier-free matrix
• Example: $\forall x \exists y \forall z \exists w P(x, y, z, w)$ can be converted to $\forall x \forall z P(x, f(x), z, g(x, z))$, where $f$ and $g$ are Skolem functions

Conversion to Clausal Normal Form

Converting the Matrix to Conjunctive Normal Form

• To convert a formula in Skolem normal form into clausal normal form, first convert the matrix of the formula into conjunctive normal form (CNF)
• Use the following equivalence rules to convert the matrix into CNF:
  • Eliminate implications ($A \rightarrow B \equiv \neg A \vee B$) and bi-implications ($A \leftrightarrow B \equiv (A \rightarrow B) \wedge (B \rightarrow A)$)
  • Move negations inward using De Morgan's laws ($\neg (A \wedge B) \equiv \neg A \vee \neg B$ and $\neg (A \vee B) \equiv \neg A \wedge \neg B$) and double negation elimination ($\neg \neg A \equiv A$)
  • Distribute disjunctions over conjunctions using the distributive law ($A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$)
• Example: $\forall x (P(x) \rightarrow (Q(x) \wedge R(x)))$ can be converted to $\forall x ((\neg P(x) \vee Q(x)) \wedge (\neg P(x) \vee R(x)))$

Representing Clauses as Sets of Literals

• After converting the matrix into CNF, the formula will consist of a conjunction of clauses, where each clause is a disjunction of literals
• Drop the universal quantifiers from the formula, as they are implicit in clausal normal form
• Represent the conjunction of clauses as a set of clauses, and each clause as a set of literals
• The resulting set of clauses is the clausal normal form of the original formula
• Example: $\forall x \forall y ((P(x) \vee Q(y)) \wedge (\neg P(x) \vee R(y)))$ can be represented as $\{\{P(x), Q(y)\}, \{\neg P(x), R(y)\}\}$ in clausal normal form