orbital.moon.logic
Class ClassicalLogic.Utilities

java.lang.Object
  orbital.moon.logic.ClassicalLogic.Utilities

Enclosing class:

ClassicalLogic

public static final class ClassicalLogic.Utilities
extends java.lang.Object

Formula transformation utilities.

Author:

André Platzer

See Also:

Utility

Stereotype:

Utilities, Module

Field Summary

static java.util.Set

CONTRADICTION Deprecated. Use Clause.CONTRADICTION instead.

Method Summary

static java.util.Set	clausalForm(Formula f, boolean simplifying) Deprecated. Prefer to use the more general method ClausalFactory.asClausalSet(orbital.logic.imp.Formula) instead.
static Formula	conjunctiveForm(Formula f) Transforms into conjunctive normal form (CNF).
static Formula	conjunctiveForm(Formula f, boolean simplifying) Transforms into conjunctive normal form (CNF).
static Formula	constantClosure(Formula F) Get the constant-closure of a formula.
static Formula	disjunctiveForm(Formula f) Transforms into disjunctive normal form (DNF).
static Formula	disjunctiveForm(Formula f, boolean simplifying) Transforms into disjunctive normal form (DNF).
static Formula	dropQuantifiers(Formula F) Drop any quantifiers.
static Formula	existentialClosure(Formula F) Get the ∃-closure of a formula.
static Formula	negation(Formula F) Get the negation of F without introducing duplex negatios.
static Formula	negationForm(Formula F) Get the negation normal form of a formula.
static Formula	skolemForm(Formula F) Get the Skolem normal form of a formula.
static Formula	universalClosure(Formula F) Get the ∀-closure of a formula.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

CONTRADICTION

public static final java.util.Set CONTRADICTION

Deprecated. Use Clause.CONTRADICTION instead.

The contradictory clause ∅ ≡ □ ≡ ⊥.

The contradictory set of clauses is {∅}={□} while the tautological set of clauses is {}.

Method Detail

disjunctiveForm

public static Formula disjunctiveForm(Formula f)

Transforms into disjunctive normal form (DNF).

See Also:

disjunctiveForm(Formula,boolean)

disjunctiveForm

public static Formula disjunctiveForm(Formula f,
                                      boolean simplifying)

Transforms into disjunctive normal form (DNF).

Note that the conversion to equivalent DNF is inherently exponential in the length of the formulas.

	SAT	Tautology
CNF	NP-complete	linear
DNF	linear	Co-NP-complete

This TRS terminates but is not confluent, hence it does not lead to a canonical form. The canonical form would not be minimal, though.

Parameters:

simplifying - Whether to enable simplifying transformations. Observe that, to avoid complexity pitfalls, this will perform partial simplification during the transformation. For performance reasons, the implementation avoids a full simplification.

See Also:

"Rolf Socher-Ambrosius. Boolean algebra admits no convergent term rewriting system, Springer Lecture Notes in Computer Science 488, RTA '91."

Preconditions:

true

Postconditions:

RES ≡ f

Attributes:

time complexity exponential

conjunctiveForm

public static Formula conjunctiveForm(Formula f)

Transforms into conjunctive normal form (CNF).

See Also:

conjunctiveForm(Formula, boolean)

conjunctiveForm

public static Formula conjunctiveForm(Formula f,
                                      boolean simplifying)

Transforms into conjunctive normal form (CNF).

Note that the conversion to equivalent CNF is inherently exponential in the length of the formulas.

	SAT	Tautology
CNF	NP-complete	linear
DNF	linear	Co-NP-complete

This TRS terminates but is not confluent, hence it does not lead to a canonical form. The canonical form would not be minimal, though.

Parameters:

simplifying - Whether to enable simplifying transformations. Observe that, to avoid complexity pitfalls, this will perform partial simplification during the transformation. For performance reasons, the implementation avoids a full simplification. If you need even more simplification, use ClausalFactory.asClausalSet(orbital.logic.imp.Formula) instead. clausalFactory.asClausalSet().toFormula();

See Also:

ClausalFactory.asClausalSet(orbital.logic.imp.Formula), "David A. Plaisted & Steven Greenbaum. A structure-preserving clause form translation. J. Symb. Comput., Academic Press, Inc., 1986, 2, 293-304.", "Rolf Socher-Ambrosius. Boolean algebra admits no convergent term rewriting system, Springer Lecture Notes in Computer Science 488, RTA '91."

Preconditions:

true

Postconditions:

RES ≡ f

Attributes:

time complexity exponential

negationForm

public static final Formula negationForm(Formula F)

Get the negation normal form of a formula.

A formula is in a negation normal form if the only negations are due to literals, i.e. negations may only occur directly in front of an atom.

In order to prevent ill-defined negation normal forms, we will first get rid of derived junctors like →,↔ etc.

clausalForm

public static final java.util.Set clausalForm(Formula f,
                                              boolean simplifying)

Deprecated. Prefer to use the more general method ClausalFactory.asClausalSet(orbital.logic.imp.Formula) instead.

Transforms into clausal form.

Defined per structural induction.

Parameters:

simplifying - Whether or not to use simplified CNF for calculating clausal forms.

See Also:

ClausalFactory.asClausalSet(orbital.logic.imp.Formula)

dropQuantifiers

public static final Formula dropQuantifiers(Formula F)

Drop any quantifiers. Will simply remove every quantifier from F.

skolemForm

public static final Formula skolemForm(Formula F)

Get the Skolem normal form of a formula.

After transforming F into negation normal form, a Skolem normal form can be constructed per

• sk(A) = A if A is a literal
• sk(A∧B) = sk(A)∧sk(B)
• sk(A∨B) = sk(A)∨sk(B)
• sk(∀x A) = ∀x sk(A)
• sk(∃x A) = sk(A[x→f(x₁,...,x_n)]) where FV(∃x A) = {x₁,...,x_n}
• sk(∃λx A) = sk((λx A)(f(x₁,...,x_n))) where FV(∃λx A) = {x₁,...,x_n}

Skolemization is ∀x∃y φ ≅ ∃F∀x φ[y↦F(x)] usually with the satisfiability-equivalent transformation "constantify" to ∀x φ[y↦f(x)]

This method will call negationForm(Formula).

universalClosure

public static final Formula universalClosure(Formula F)

Get the ∀-closure of a formula.

Parameters:

F - the formula having free variables FV(F)=:{x₁,...,x_n}.

Returns:

the universal closure Cl_∀F = ∀x₁...∀x_n F

See Also:

existentialClosure(Formula), constantClosure(Formula)

Postconditions:

RES.getFreeVariables()=∅ ∧ RES=F.getFreeVariables()->iterate(x;G=F;G=G.forall(x))

existentialClosure

public static final Formula existentialClosure(Formula F)

Get the ∃-closure of a formula.

Parameters:

F - the formula having free variables FV(F)=:{x₁,...,x_n}.

Returns:

the existential closure Cl_∃F = ∃x₁...∃x_n F

See Also:

universalClosure(Formula), constantClosure(Formula)

Postconditions:

RES.getFreeVariables()=∅ ∧ RES=F.getFreeVariables()->iterate(x;G=F;G=G.exist(x))

constantClosure

public static final Formula constantClosure(Formula F)

Get the constant-closure of a formula.

This method replaces all free variables by constants of the same signifier, type and notation. Especially, in combination with other formulas of the same free variables, the closure constants will be the same, unlike any skolem constants introduced in the &exists;-closures of those formulas.

Parameters:

F - the formula having free variables FV(F)=:{x₁,...,x_n}.

Returns:

the constant closure Cl_constF = F[x₁→x₁,...,x_n→x_n]

See Also:

existentialClosure(Formula), universalClosure(Formula)

Postconditions:

RES.getFreeVariables()=∅ ∧ RES=...

negation

public static final Formula negation(Formula F)

Get the negation of F without introducing duplex negatios.

Returns:

G if F=¬G, and ¬F otherwise.

Preconditions:

F==ClassicalLogic.conjunctiveForm(F)

Postconditions:

RES==ClassicalLogic.conjunctiveForm(F.not())