orbital.moon.logic.resolution
Interface ClausalSet

All Superinterfaces:

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

All Known Implementing Classes:

ClausalSetImpl, IndexedClausalSetImpl

public interface ClausalSet
extends java.util.Set

Represents a set of clauses. A set of clauses {C₁,...,C_n} is a different notation for the conjunction C₁∧...∧C_n. This set representation already incorporates associative and commutative.

Author:

André Platzer

Field Summary

static ClausalSet	CONTRADICTION_SINGLETON_SET The contradictory singleton set of clauses {□}.
static ClausalSet	TAUTOLOGY_SINGLETON_SET The tautological singleton set of clauses {}.

Method Summary

java.util.Iterator	getProbableComplementsOf(Clause C) Get (an iterator over) all clauses contained in this set that may possibly form a complement to C for resolution.
boolean	removeAllSubsumedBy(ClausalSet T) Remove all clauses from this set which are subsumed by any of the clauses of T.
Formula	toFormula() Convert this set of clauses to a formula representation.

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_SINGLETON_SET

static final ClausalSet CONTRADICTION_SINGLETON_SET

The contradictory singleton set of clauses {□}.

TAUTOLOGY_SINGLETON_SET

static final ClausalSet TAUTOLOGY_SINGLETON_SET

The tautological singleton set of clauses {}.

Method Detail

removeAllSubsumedBy

boolean removeAllSubsumedBy(ClausalSet T)

Remove all clauses from this set which are subsumed by any of the clauses of T.

In case of T == this, don't let clauses remove by mutual subsumption, or by self-subsumption.

Returns:

whether this set has changed as a result of the deletion by subsumption.

getProbableComplementsOf

java.util.Iterator getProbableComplementsOf(Clause C)

Get (an iterator over) all clauses contained in this set that may possibly form a complement to C for resolution. The clauses returned will more likely qualify for resolution with C, but need not do so with absolute confidence.

Implementations may use indexing to estimate the clauses to return very quickly.

Postconditions:

RES⊆this ∧ RES ⊇ {D∈this ¦ ∃L∈C ∃K∈D ∃mgU{L,~K}}

toFormula

Formula toFormula()

Convert this set of clauses to a formula representation.