orbital.moon.logic.resolution
Class ClausalIndex

java.lang.Object
  orbital.moon.logic.resolution.ClausalIndex

public class ClausalIndex
extends java.lang.Object

Manages a clause index.

Author:

André Platzer

Constructor Summary

ClausalIndex()
Create a new empty index.

Method Summary

boolean	add(Clause C) Add clause C to our index.
void	clear()
java.util.Iterator	getProbableComplementClauses(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with ~L.
java.util.Iterator	getProbableComplementLiterals(Formula L) Get an iterator of all literals which could possibly unify with ~L.
java.util.Iterator	getProbableComplements(Formula L) Get an iterator of all (clause,literal) pairs which could possibly unify with ~L.
java.util.Iterator	getProbableUnifiableClauses(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with L.
java.util.Iterator	getProbableUnifiableLiterals(Formula L) Get an iterator of all literals which could possibly unify with L.
java.util.Iterator	getProbableUnifiables(Formula L) Get an iterator of all (clause,literal) pairs which could possibly unify with L.
boolean	isEmpty() Check whether this index is empty.
boolean	remove(Clause C) Remove clause C from our index.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

ClausalIndex

public ClausalIndex()

Create a new empty index.

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getProbableUnifiables

public java.util.Iterator getProbableUnifiables(Formula L)

Get an iterator of all (clause,literal) pairs which could possibly unify with L.

Postconditions:

RES = {(C,K)∈this ¦ K∈C ∧ possibly ∃mgU{L,K}}

getProbableComplements

public java.util.Iterator getProbableComplements(Formula L)

Get an iterator of all (clause,literal) pairs which could possibly unify with ~L.

Postconditions:

RES = getProbableUnifiables(ClassicalLogic.Utilities.negation(L))

getProbableUnifiableClauses

public java.util.Iterator getProbableUnifiableClauses(Formula L)

Get an iterator of all clauses that contain literals which could possibly unify with L.

getProbableComplementClauses

public java.util.Iterator getProbableComplementClauses(Formula L)

Get an iterator of all clauses that contain literals which could possibly unify with ~L.

getProbableUnifiableLiterals

public java.util.Iterator getProbableUnifiableLiterals(Formula L)

Get an iterator of all literals which could possibly unify with L.

getProbableComplementLiterals

public java.util.Iterator getProbableComplementLiterals(Formula L)

Get an iterator of all literals which could possibly unify with ~L.

isEmpty

public boolean isEmpty()

Check whether this index is empty.

add

public boolean add(Clause C)

Add clause C to our index. Adds C to all indices of literals in C.

Returns:

whether the index changed as a result of this operation.

remove

public boolean remove(Clause C)

Remove clause C from our index. Removes C from all indices of literals in C.

Returns:

whether the index changed as a result of this operation.

clear

public void clear()