orbital.moon.logic.resolution
Interface Clause

All Superinterfaces:

java.util.Collection, java.lang.Iterable, java.util.Set

All Known Implementing Classes:

ClauseImpl, IndexedClauseImpl, OrderedClauseImpl

public interface Clause
extends java.util.Set

Represents a clause, i.e. a set of literals. The individual literals, i.e. positive or negated atoms are ordinary formulas. This set representation already incorporates associative and commutative.

Author:

André Platzer

Field Summary

static Clause

CONTRADICTION The contradictory clause ∅ ≡ □ ≡ ⊥.

Method Summary

java.util.Iterator	factorize() Get all factors of F.
Signature	getFreeVariables() Get the free variables of a formula represented as a clause.
java.util.Iterator	getProbableUnifiables(Formula L) Get (an iterator over) all literals contained in this clause that may possibly unify with L.
java.util.Iterator	getResolvableLiterals() Select some literals of this clause, which are usable for resolution.
java.util.Set	getUnifiables(Formula L) Get all literals contained in this clause that unify with L.
boolean	isElementaryValid() Returns true when this clause obviously is an elementary tautology.
boolean	isElementaryValidUnion(Clause G) Returns true when the union F∪G would obviously contain an elementary tautology.
java.util.Iterator	resolveWith(Clause G) Get all resolvents of F and G, if any.
java.util.Iterator	resolveWithFactors(Clause G) Get all resolvents of factors of F and G, if any.
java.util.Iterator	resolveWithVariant(Clause G) Get all resolvents of variants of F and G, if any.
boolean	subsumes(Clause D) Returns true when this clause subsumes D.
Formula	toFormula() Convert this clause to a formula representation.
Clause	variant(Signature disjointify) Get a variant of this clause with the given variables renamed.

Methods inherited from interface java.util.Set

add, addAll, clear, contains, containsAll, equals, hashCode, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray

Field Detail

CONTRADICTION

static final Clause CONTRADICTION

The contradictory clause ∅ ≡ □ ≡ ⊥.

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

Method Detail

getFreeVariables

Signature getFreeVariables()

Get the free variables of a formula represented as a clause.

Returns:

freeVariables(this)

variant

Clause variant(Signature disjointify)

Get a variant of this clause with the given variables renamed. α-conversion

Parameters:

disjointify - the variables to rename (in order to produce a variable disjoint variant of F relative to some formula G).

Returns:

a variant (i.e. resulting from a variable renaming) of this clause containing no variable of the signature disjointify.

Postconditions:

RES.getFreeVariables().intersection(disjointify).isEmpty() ∧ RES is a variant of this

resolveWith

java.util.Iterator resolveWith(Clause G)

Get all resolvents of F and G, if any. (Resolution rule) Implementation already incorporates some cuts.

Returns:

an iterator over the set of all resolvent clauses.

resolveWithVariant

java.util.Iterator resolveWithVariant(Clause G)

Get all resolvents of variants of F and G, if any. (Resolution rule) Combines resolution and the required forming of variants beforehand.

See Also:

variant(Signature), resolveWith(Clause), Convenience Method

resolveWithFactors

java.util.Iterator resolveWithFactors(Clause G)

Get all resolvents of factors of F and G, if any. (Resolution rule) Combines resolution and factorization, resulting in a quicker implementation. When F can be resolved with G via the resolution literals L and K, then in addition to the ordinary resolvent, this method also returns all resolvents resulting from a factorization of F (involving L) or G (involving K). Other factorizations are not necessary for completeness, since they can be performed later during resolution over the participating literals.

See Also:

factorize(), resolveWith(Clause)

factorize

java.util.Iterator factorize()

Get all factors of F. (factorization rule).

Will implement the factorization rule necessary for binary resolution:

{L1,...,Ln} |- {s(L1),...,s(Lk)} with s=mgU({Lk,...,Ln})

Which is the same as

{L1,...,Ln} |- {s(L1),...,s(Ln)} with s=mgU({Lk,...,Ln})

because of the set representation, and which again is the same as

{L1,...,Ln} |- {s(L1),...,s(Ln)} with s=mgU({Li,Lj})

because of set notation. The latter is the way we (currently) implement things.

Returns:

all (proper) factor clauses of this, or ∅ if no factorization was possible.

subsumes

boolean subsumes(Clause D)

Returns true when this clause subsumes D. That is there is a subsitution σ such that Cσ ⊆ D (and |C| ≤ |D|).

We can forget about subsumed clause D for resolving false, and work on C instead.

Preconditions:

true

Note:

Conservative estimations are possible, i.e. returning false even for subsumption cases is allowed.

isElementaryValid

boolean isElementaryValid()

Returns true when this clause obviously is an elementary tautology. That is a p∨¬p ∈ F

We can forget about elementary valid clauses for resolving false, because true formulas will only imply true formulas, never false ones.

Preconditions:

true

Attributes:

derived isElementaryValidUnion(Clause)

isElementaryValidUnion

boolean isElementaryValidUnion(Clause G)

Returns true when the union F∪G would obviously contain an elementary tautology. That is a p∨¬p ∈ F∪G

We can forget about elementary valid clauses for resolving false, (essentially) because true formulas will only imply true formulas, never false ones.

Parameters:

G - a clause

Preconditions:

(¬this.isElementaryValid() ∧ ¬G.isElementaryValid()) ∨ F=G

getResolvableLiterals

java.util.Iterator getResolvableLiterals()

Select some literals of this clause, which are usable for resolution.

Postconditions:

RES ⊆ this

getProbableUnifiables

java.util.Iterator getProbableUnifiables(Formula L)

Get (an iterator over) all literals contained in this clause that may possibly unify with L. The formulas returned will more likely qualify for unification with C, but need not do so with absolute confidence.

Implementations may use indexing or links to estimate the clauses to return very quickly. Furthermore, implementations may apply selection refinements.

See Also:

getUnifiables(Formula)

Postconditions:

RES⊆this ∧ RES⊇getUnifiables(L)

getUnifiables

java.util.Set getUnifiables(Formula L)

Get all literals contained in this clause that unify with L.

Implementations may use indexing or links to estimate the clauses to return very quickly. Furthermore, implementations may apply selection refinements.

See Also:

getProbableUnifiables(Formula)

Postconditions:

RES = {K∈this ∃mgU{L,K}}

toFormula

Formula toFormula()

Convert this clause to a formula representation.