Interface | Description |
---|---|
ComplexRuleMap.ComplexRuleVisitor<Data,ResType> | |
Prover |
A general interface for specifying reverse provers, which start at the goal
and work backwards producing Assrts as they go.
|
Provers.UseWhenPossibleListener |
Class | Description |
---|---|
AssocComComplexRuleMap<Data> | |
AssocComTransformation |
Associative and commutative transformations
|
AssociativeInfo |
The information about associative operations.
|
AssocTree |
This tree represents associative structure
|
CanonicalOperandHelper | |
ClosureInfo | |
ClosureInfo.TemplDetectRes | |
CommutativeInfo |
The information about commutative operations.
|
CommutativeTransformation |
Only commutative transformations
|
ComplexRuleMap<Data> |
This class implements complex rule map.
|
ConjunctionInfo | |
ConstSubst | |
DBInfo | |
EquivalenceInfo |
This class is used for equivalence transformations.
|
GenProofStepStmt |
This class describes generalized proof step statement.
|
ImplicationInfo |
This class is used for implication transformations.
|
ImplicationInfo.ExtractImplResult | |
ParseNodeHashElem | |
Pattern | |
PropertyTemplate |
The template for some property.
|
Prover.AssrtProver |
A general interface for specifying reverse provers, which start at the
goal and work backwards producing Assrts as they go.
|
Prover.HypProver |
An extension to
Prover , where the function is only required to
give an Assrt and substitutions to the variables in the Assrt. |
Prover.HypProverResult |
Result type for a
Prover.HypProver . |
Prover.ProverResult | |
Provers | |
Provers.ArrayProver | |
Provers.UseWhenPossible |
A Prover which uses the given assrt whenever it matches the current goal.
|
ReplaceInfo | |
ReplaceTransformation |
The replace transformation: we could transform children of corresponding node
and replace them with its canonical form (or vice versa).
|
Transformation |
The transformation of
Transformation.originalNode to any equal node. |
TransformationManager |
This contains information for possible automatic transformations.
|
TrConstants |
(Most) Constants used in mmj.transforms classes
|
TrOutput | |
TrUtil |
Enum | Description |
---|---|
ClosureInfo.ClosureResult |