Package | Description |
---|---|
jtabwb.engine |
Main classes implementing the engine; it specifies the interfaces with the
user defined prover.
|
jtabwb.launcher |
Implementation of a command line launcher for provers.
|
jtabwb.tracesupport |
Some tool for managing traces and C-trees, including support for LaTeX source
generation.
|
Modifier and Type | Method and Description |
---|---|
_Prover |
Trace.getProver()
Returns the prover used to generate this trace.
|
Constructor and Description |
---|
Engine(_Prover prover,
_AbstractGoal goal)
Builds an instance of the engine act that allows to search for a proof of
the goal specified as argument (initial goal) using the specified
prover.
|
Engine(_Prover prover,
_AbstractGoal goal,
Engine.ExecutionMode mode)
Builds an instance of the engine act that allows to search for a proof of
the goal specified as argument (initial goal) using the specified
prover.
|
Modifier and Type | Method and Description |
---|---|
<T extends _Prover> |
Launcher.configTheoremProver(java.lang.String name,
java.lang.Class<T> prover)
Adds to this launcher a theorem prover with the specified name and
implementation.
|
<T extends _Prover> |
Launcher.configTheoremProver(java.lang.String name,
java.lang.Class<T> prover,
boolean isDefault)
Adds a theorem prover with the specified name and implementation to this
launcher specifying if it is (
isDefault==true ) or not (
isDefault==false ) the default prover for this launcher. |
Modifier and Type | Method and Description |
---|---|
_Prover |
ProofSearchData.getProver()
Returns the proved used to perform the proof-search.
|
Modifier and Type | Method and Description |
---|---|
java.lang.Class<_Prover> |
ConfiguredTheoremProver.getValue()
Returns the class of the prover.
|
Modifier and Type | Method and Description |
---|---|
void |
_SingleExecutionConfigurator.configProver(_Prover prover,
_AbstractGoal initialGoal,
Launcher.LaunchConfiguration currentLauncherConfiguration)
This method is executed by the launcher immediately before invoking
_InitialGoalBuilder.buildInitialNodeSet(ProblemDescription) . |
Constructor and Description |
---|
ConfiguredTheoremProver(java.lang.String name,
java.lang.String description,
java.lang.Class<_Prover> value) |
Modifier and Type | Class and Description |
---|---|
class |
Validator |
Modifier and Type | Method and Description |
---|---|
_Prover |
TraceValidator.getProver() |
_Prover |
CTree.getProver()
Returns the prover that generated the C-tree.
|
Constructor and Description |
---|
TraceValidator(Trace trace,
_Prover prover,
_TraceSupport traceSupport) |
Validator(Trace trace,
_Prover prover,
_TraceManager traceManager) |