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.

• ClassicalLogic is an implementation of classical first-order logic. Once instantiated, it is best accessed through its interface orbital.logic.imp.Logic.