
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
public interface Clause
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.
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 

static final Clause CONTRADICTION
The contradictory singleton set of clauses
is {∅}={□}
while the tautological set of clauses is {}.
Method Detail 

Signature getFreeVariables()
Clause variant(Signature disjointify)
disjointify
 the variables to rename (in order to produce a variable disjoint variant of F relative to some formula G).
disjointify
.java.util.Iterator resolveWith(Clause G)
java.util.Iterator resolveWithVariant(Clause G)
variant(Signature)
,
resolveWith(Clause)
,
Convenience Methodjava.util.Iterator resolveWithFactors(Clause G)
factorize()
,
resolveWith(Clause)
java.util.Iterator factorize()
Will implement the factorization rule necessary for binary resolution:
∅
if no factorization was possible.boolean subsumes(Clause D)
We can forget about subsumed clause D for resolving false, and work on C instead.
boolean isElementaryValid()
We can forget about elementary valid clauses for resolving false, because true formulas will only imply true formulas, never false ones.
isElementaryValidUnion(Clause)
boolean isElementaryValidUnion(Clause G)
We can forget about elementary valid clauses for resolving false, (essentially) because true formulas will only imply true formulas, never false ones.
G
 a clausejava.util.Iterator getResolvableLiterals()
java.util.Iterator getProbableUnifiables(Formula L)
Implementations may use indexing or links to estimate the clauses to return very quickly. Furthermore, implementations may apply selection refinements.
getUnifiables(Formula)
java.util.Set getUnifiables(Formula L)
Implementations may use indexing or links to estimate the clauses to return very quickly. Furthermore, implementations may apply selection refinements.
getProbableUnifiables(Formula)
Formula toFormula()

Orbital library 1.3.0: 11 Apr 2009 

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 