Orbital library

orbital.moon.logic.resolution
Class ClauseImpl

java.lang.Object
  extended by java.util.AbstractCollection
      extended by java.util.AbstractSet
          extended by java.util.HashSet
              extended by java.util.LinkedHashSet
                  extended by 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 {L1,...,Ln} is a different notation for the disjunction L1∨...∨Ln.

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

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.