Orbital library

Package orbital.moon.logic.resolution

Provides resolution inference theorem prover implementation and clause management.

See:
          Description

Interface Summary
ClausalFactory Factory for clauses and clausal sets.
ClausalSet Represents a set of clauses.
Clause Represents a clause, i.e.
 

Class Summary
ClausalIndex Manages a clause index.
ClausalSetImpl Default implementation of a representation of a set of clauses.
ClauseImpl Default implementation of a representation of a clause, i.e.
DefaultClausalFactory Factory for clauses and clausalsets.
IndexedClausalSetImpl Implementation of a representation of a set of clauses with clause indexing.
IndexedClauseImpl Implementation of a representation of a clauses with clause indexing.
LiteralOrders Provides literal L-orders.
OrderedClauseImpl Implementation of a representation of a clause performing ordered resolution.
ResolutionBase Basic skeleton for resolution theorem provers.
SaturationResolution Naïve saturation.
SearchResolution Set of support resolution based on search.
SetOfSupportResolution Direct set of support resolution.
 

Package orbital.moon.logic.resolution Description

Provides resolution inference theorem prover implementation and clause management.

This is an implementation package and it is usually sufficient to use the high level interface ClassicalLogic.


Orbital library
1.3.0: 11 Apr 2009

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