| Home | Trees | Indices | Help |
|
|---|
|
|
Interfaces and base classes for theorem provers and model builders.
Prover is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.
ModelBuilder is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal G, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of G.
|
|||
|
Prover Interface for trying to prove a goal from assumptions. |
|||
|
ModelBuilder Interface for trying to build a model of set of formulas. |
|||
|
TheoremToolCommand This class holds a goal and a list of assumptions to be used in proving or model building. |
|||
|
ProverCommand This class holds a Prover, a goal, and a list of
assumptions.
|
|||
|
ModelBuilderCommand This class holds a ModelBuilder, a goal, and a list of
assumptions.
|
|||
|
BaseTheoremToolCommand This class holds a goal and a list of assumptions to be used in proving or model building. |
|||
|
BaseProverCommand This class holds a Prover, a goal, and a list of
assumptions.
|
|||
|
BaseModelBuilderCommand This class holds a ModelBuilder, a goal, and a list of
assumptions.
|
|||
|
TheoremToolCommandDecorator A base decorator for the ProverCommandDecorator and
ModelBuilderCommandDecorator classes from which
decorators can extend.
|
|||
|
ProverCommandDecorator A base decorator for the ProverCommand class from
which other prover command decorators can extend.
|
|||
|
ModelBuilderCommandDecorator A base decorator for the ModelBuilderCommand class
from which other prover command decorators can extend.
|
|||
|
ParallelProverBuilder This class stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. |
|||
|
ParallelProverBuilderCommand This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. |
|||
| TheoremToolThread | |||
| Home | Trees | Indices | Help |
|
|---|
| Generated by Epydoc 3.0.1 on Mon Apr 11 14:39:41 2011 | http://epydoc.sourceforge.net |