orbital.moon.logic.resolution
Class ClauseImpl

java.lang.Object
  java.util.AbstractCollection
      java.util.AbstractSet
          java.util.HashSet
              java.util.LinkedHashSet
                  orbital.moon.logic.resolution.ClauseImpl

All Implemented Interfaces:

java.io.Serializable, java.lang.Cloneable, java.lang.Iterable, java.util.Collection, java.util.Set, Clause

Direct Known Subclasses:

IndexedClauseImpl

public class ClauseImpl
extends java.util.LinkedHashSet
implements Clause

Default implementation of a representation of a clause, i.e. a set of literals. A clause {L₁,...,L_n} is a different notation for the disjunction L₁∨...∨L_n.

Author:

André Platzer

See Also:

Serialized Form

Field Summary

Fields inherited from interface orbital.moon.logic.resolution.Clause

CONTRADICTION

Constructor Summary

ClauseImpl()

ClauseImpl(java.util.Set literals)
Copy constructor.

Method Summary

java.util.Iterator	factorize() Get all factors of F.
protected Clause	factorize(java.util.Collection literals) Factorize a clause by the specified literals.
protected Pair	factorize2(java.util.Collection literals) Workaround for returning 2 arguments.
protected static ClausalFactory	getClausalFactory()
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.
protected Clause	resolventWith(Clause G, Formula L, Formula K) Resolve clause F with G by the complementary resolution literals L∈F and K∈G.
protected Pair	resolventWith2(Clause G, Formula L, Formula K) Workaround for returning 2 arguments.
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.
java.util.Iterator	resolveWithVariantFactors(Clause G)
boolean	subsumes(Clause D) Implements subsumption based on unit input semi-ground resolution.
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 class java.util.HashSet

add, clear, clone, contains, isEmpty, iterator, remove, size

Methods inherited from class java.util.AbstractSet

equals, hashCode, removeAll

Methods inherited from class java.util.AbstractCollection

addAll, containsAll, retainAll, toArray, toArray, toString

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.util.Set

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

Constructor Detail

ClauseImpl

public ClauseImpl(java.util.Set literals)

Copy constructor.

ClauseImpl

public ClauseImpl()

Method Detail

getClausalFactory

protected static ClausalFactory getClausalFactory()

getFreeVariables

public Signature getFreeVariables()

Description copied from interface: Clause

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

Specified by:

getFreeVariables in interface Clause

Returns:

freeVariables(this)

resolveWith

public java.util.Iterator resolveWith(Clause G)

Description copied from interface: Clause

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

Specified by:

resolveWith in interface Clause

Returns:

an iterator over the set of all resolvent clauses.

resolveWithFactors

public java.util.Iterator resolveWithFactors(Clause _G)

Description copied from interface: Clause

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.

Specified by:

resolveWithFactors in interface Clause

See Also:

Clause.factorize(), Clause.resolveWith(Clause)

resolventWith

protected Clause resolventWith(Clause G,
                               Formula L,
                               Formula K)

Resolve clause F with G by the complementary resolution literals L∈F and K∈G.

Returns:

the resolvent ((F\{L})∪(G\{K}))μ when ∃μ∈mgU{L,¬K}. Or null if the resolution of F with G by L and K is impossible because of mgU{L,¬K}=∅.

Preconditions:

this.contains(L) ∧ G.contains(K)

resolventWith2

protected Pair resolventWith2(Clause G,
                              Formula L,
                              Formula K)

Workaround for returning 2 arguments.

Returns:

the pair of substitution and resulting clause, respectively (null,null).

variant

public Clause variant(Signature disjointify)

Description copied from interface: Clause

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

Specified by:

variant in interface Clause

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.

resolveWithVariant

public java.util.Iterator resolveWithVariant(Clause G)

Description copied from interface: Clause

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

Specified by:

resolveWithVariant in interface Clause

See Also:

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

resolveWithVariantFactors

public java.util.Iterator resolveWithVariantFactors(Clause G)

isElementaryValidUnion

public boolean isElementaryValidUnion(Clause G)

Description copied from interface: Clause

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.

Specified by:

isElementaryValidUnion in interface Clause

Parameters:

G - a clause

isElementaryValid

public boolean isElementaryValid()

Description copied from interface: Clause

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.

Specified by:

isElementaryValid in interface Clause

factorize

public java.util.Iterator factorize()

Description copied from interface: Clause

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.

Specified by:

factorize in interface Clause

Returns:

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

factorize

protected Clause factorize(java.util.Collection literals)

Factorize a clause by the specified literals.

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.

Parameters:

literals - the literals {Lk,...,Ln} to factorize to a single literal.

Returns:

the factorized clause, or null if no factorization was possible.

Preconditions:

this.containsAll(literals)

factorize2

protected Pair factorize2(java.util.Collection literals)

Workaround for returning 2 arguments.

Returns:

the pair of substitution and resulting factor, respectively (null,null).

subsumes

public boolean subsumes(Clause D)

Implements subsumption based on unit input semi-ground resolution.

Specified by:

subsumes in interface Clause

getResolvableLiterals

public java.util.Iterator getResolvableLiterals()

Description copied from interface: Clause

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

Specified by:

getResolvableLiterals in interface Clause

getProbableUnifiables

public java.util.Iterator getProbableUnifiables(Formula L)

Description copied from interface: Clause

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.

Specified by:

getProbableUnifiables in interface Clause

See Also:

Clause.getUnifiables(Formula)

getUnifiables

public java.util.Set getUnifiables(Formula L)

Description copied from interface: Clause

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.

Specified by:

getUnifiables in interface Clause

See Also:

Clause.getProbableUnifiables(Formula)

toFormula

public Formula toFormula()

Description copied from interface: Clause

Convert this clause to a formula representation.

Specified by:

toFormula in interface Clause