orbital.moon.logic.resolution
Class OrderedClauseImpl

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

All Implemented Interfaces:

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

public class OrderedClauseImpl
extends IndexedClauseImpl

Implementation of a representation of a clause performing ordered resolution.

Author:

André Platzer

See Also:

Serialized Form

Field Summary

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

CONTRADICTION

Constructor Summary

OrderedClauseImpl()

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

Method Summary

boolean	add(java.lang.Object o)
void	clear()
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.Iterator	iterator()
boolean	remove(java.lang.Object o)
protected Clause	resolventWith(Clause _G, Formula L, Formula K) Resolve clause F with G by the complementary resolution literals L∈F and K∈G.

Methods inherited from class orbital.moon.logic.resolution.ClauseImpl

factorize, factorize, factorize2, getClausalFactory, getFreeVariables, getUnifiables, isElementaryValid, isElementaryValidUnion, resolventWith2, resolveWith, resolveWithFactors, resolveWithVariant, resolveWithVariantFactors, subsumes, toFormula, variant

Methods inherited from class java.util.HashSet

clone, contains, isEmpty, 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

addAll, contains, containsAll, equals, hashCode, isEmpty, removeAll, retainAll, size, toArray, toArray

Constructor Detail

OrderedClauseImpl

public OrderedClauseImpl(java.util.Set literals)

Copy constructor.

OrderedClauseImpl

public OrderedClauseImpl()

Method Detail

resolventWith

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

Description copied from class: ClauseImpl

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

Overrides:

resolventWith in class ClauseImpl

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}=∅.

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

Overrides:

getResolvableLiterals in class ClauseImpl

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

Overrides:

getProbableUnifiables in class IndexedClauseImpl

See Also:

Clause.getUnifiables(Formula)

add

public boolean add(java.lang.Object o)

Specified by:

add in interface java.util.Collection

Specified by:

add in interface java.util.Set

Overrides:

add in class IndexedClauseImpl

clear

public void clear()

Specified by:

clear in interface java.util.Collection

Specified by:

clear in interface java.util.Set

Overrides:

clear in class IndexedClauseImpl

remove

public boolean remove(java.lang.Object o)

Specified by:

remove in interface java.util.Collection

Specified by:

remove in interface java.util.Set

Overrides:

remove in class IndexedClauseImpl

iterator

public java.util.Iterator iterator()

Specified by:

iterator in interface java.lang.Iterable

Specified by:

iterator in interface java.util.Collection

Specified by:

iterator in interface java.util.Set

Overrides:

iterator in class IndexedClauseImpl