Orbital library

orbital.moon.logic.resolution
Class ClausalIndex

java.lang.Object
  extended by 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()

Orbital library
1.3.0: 11 Apr 2009

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