Package org.semanticweb.HermiT.tableau

Interface Summary
DependencySet  
DLClauseEvaluator.BranchingWorker  
DLClauseEvaluator.Worker  
ExtensionTable.CoreManager  
ExtensionTable.DependencySetManager  
ExtensionTable.Retrieval  
 

Class Summary
BranchingPoint Represents a branching point for the tableau given to the constructor.
ClashManager An instance of this class is notified by extension tables when tuples are added.
DatatypeManager  
DatatypeManager.DConjunction  
DatatypeManager.DVariable  
DatatypeManager.SmallestEnumerationFirst  
DependencySetFactory This is the main class to work with dependency sets and returns instances of PermanentDependencySet, which can not directly be created.
DependencySetFactory.IntegerArray  
DescriptionGraphManager  
DescriptionGraphManager.OccurrenceManager  
DisjunctionBranchingPoint  
DLClauseEvaluator  
DLClauseEvaluator.BranchIfNotEqual  
DLClauseEvaluator.BranchIfNotNodeIDLessEqualThan  
DLClauseEvaluator.BranchIfNotNodeIDsAscendingOrEqual  
DLClauseEvaluator.BufferSupply  
DLClauseEvaluator.CallMatchFinishedOnMonitor  
DLClauseEvaluator.CallMatchStartedOnMonitor  
DLClauseEvaluator.CopyDependencySet  
DLClauseEvaluator.CopyValues  
DLClauseEvaluator.DeriveBinaryFact  
DLClauseEvaluator.DeriveDisjunction  
DLClauseEvaluator.DeriveTernaryFact  
DLClauseEvaluator.DeriveUnaryFact  
DLClauseEvaluator.DLClauseCompiler  
DLClauseEvaluator.GroundDisjunctionHeaderManager  
DLClauseEvaluator.HasMoreRetrieval  
DLClauseEvaluator.JumpTo  
DLClauseEvaluator.NextRetrieval  
DLClauseEvaluator.OpenRetrieval  
DLClauseEvaluator.SetClash  
DLClauseEvaluator.ValuesBufferManager  
ExistentialExpansionManager Manages the expansion of at least restrictions in a tableau.
ExtensionManager  
ExtensionTable An extension table keeps track of the assertions in the ABox during a run of the tableau.
ExtensionTable.DeterministicDependencySetManager  
ExtensionTable.NoCoreManager  
ExtensionTable.RealCoreManager  
ExtensionTableWithFullIndex This extension table is for use with Description Graphs and it supports tuple tables with arity greater than three, but are, as a result, less efficient.
ExtensionTableWithTupleIndexes This extension table is for use with binary and ternary assertions (not description graphs).
GroundDisjunction  
GroundDisjunctionHeader  
GroundDisjunctionHeader.DisjunctIndexWithBacktrackings  
HyperresolutionManager Applies the rules during the expansion of a tableau.
HyperresolutionManager.BodyAtomsSwapper  
HyperresolutionManager.CompiledDLClauseInfo  
HyperresolutionManager.DLClauseBodyKey  
InterruptFlag  
MergingManager Implements the merge rule and is used whenever the merge rule needs to be applied during the expansion of the tableau object used in the constructor of the class.
Node Represents a node in the tableau.
NominalIntroductionManager Implements the nominal introduction rule.
PermanentDependencySet  
ReasoningTaskDescription  
Tableau This class coordinates the main tableau expansion for a given DLOntology (a normalized and clausified ontology).
TupleIndex  
TupleIndex.TrieNodeManager  
TupleIndex.TupleIndexRetrieval  
TupleTable The actual implementation of the tuple tables used in the ExtensionTable class.
TupleTable.Page  
TupleTableFullIndex  
TupleTableFullIndex.EntryManager  
UnionDependencySet  
 

Enum Summary
ExtensionTable.View  
InterruptFlag.InterruptType  
InterruptFlag.TimerState  
Node.NodeState  
NodeType  
ReasoningTaskDescription.StandardTestType  
 

Exception Summary
InterruptCurrentTaskException