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 |
---|---|
ProofSearchResult |
Engine.getResult()
Returns the result of the last proof-search.
|
ProofSearchResult |
TraceNode.getStatus() |
ProofSearchResult |
Trace.getStatus()
Returns the status of the proof-search described by this trace.
|
ProofSearchResult |
Engine.searchProof()
Searches a proof for the initial goal and, if it terminates, returns the
result of the proof-search.
|
ProofSearchResult |
_ClashDetectionRule.status()
|
static ProofSearchResult |
ProofSearchResult.valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static ProofSearchResult[] |
ProofSearchResult.values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
Modifier and Type | Method and Description |
---|---|
void |
_OnRuleCompletedListener.onCompleted(ProofSearchResult status)
Invoked by the engine when the proof-search starting with this rule
application terminates.
|
ProvabilityStatus |
_Prover.statusFor(ProofSearchResult result)
Returns the provability status corresponding to the specified proof-search
result.
|
Modifier and Type | Method and Description |
---|---|
ProofSearchResult |
ProofSearchData.getResult()
Returns the result of the proof-search.
|
Modifier and Type | Method and Description |
---|---|
ProofSearchResult |
CTreeNode.getStatus() |
ProofSearchResult |
CTree.getStatus()
Returns the status of the C-tree.
|
Modifier and Type | Method and Description |
---|---|
ProvabilityStatus |
Validator.statusFor(ProofSearchResult result) |