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.
|
jtabwbx.modal.basic |
Basic classes and interfaces for propositional modla formulas.
|
jtabwbx.modal.btformula |
A basic implementation of propositional modal formulas as binary trees.
|
jtabwbx.modal.formula |
An implementation of propositional modal formulas based on graphs.
|
jtabwbx.prop.basic |
Basic classes and interfaces for propositional formulas.
|
jtabwbx.prop.btformula |
A basic implementation of propositional formulas as binary trees.
|
jtabwbx.prop.formula |
An implementation of propositional formulas based on graphs.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
_AbstractGoal
An abstract goal represent a goal during proof-search.
|
_AbstractRule
The supertype of rules; this interface should be never implemented by itself,
but only as part of its sub-interfaces.
|
_Prover
An object realizing an instance of a prover.
|
_Strategy
The strategy defines the way the proof-search space is visited; at every
iteration the engine invokes
_Strategy.nextRule(_AbstractGoal, IterationInfo) ) to determine the rule to
apply to the current-goal of the proof-search. |
Engine.ExecutionMode
Engine execution mode flags.
|
IterationInfo
A bunch of data describing the last iteration performed by the engine.
|
IterationInfo.Move
The possible moves performed by the engine.
|
NoSuchBacktrackRuleException
Specialised version of
NoSuchElementException thrown by the
_MetaBacktrackRule.nextRule() method to indicate that there are no
more backtrack rules. |
ProofSearchResult
The result of the proof-search.
|
ProvabilityStatus
The status of an input formula.
|
ProverName
Utility class to manage the name of a prover.
|
RuleType
The type of a rule classify a rule applied during proof search.
|
Trace
A trace describes the steps performed during a proof search; it provides data
about:
the prover used to generate the proof-search;
the initial node-set of the proof-search;
the status of the proof-search;
the root of the trace-tree describing the performed proof search.
We call trace tree the tree describing the proof-search.
|
TraceException
Thrown if something goes wrong managing a trace.
|
TraceNode
A node in the proof-trace, it describes a rule applied in the proof-search.
|
Class and Description |
---|
_AbstractGoal
An abstract goal represent a goal during proof-search.
|
_Prover
An object realizing an instance of a prover.
|
ProofSearchResult
The result of the proof-search.
|
ProvabilityStatus
The status of an input formula.
|
Trace
A trace describes the steps performed during a proof search; it provides data
about:
the prover used to generate the proof-search;
the initial node-set of the proof-search;
the status of the proof-search;
the root of the trace-tree describing the performed proof search.
We call trace tree the tree describing the proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
_AbstractGoal
An abstract goal represent a goal during proof-search.
|
_AbstractRule
The supertype of rules; this interface should be never implemented by itself,
but only as part of its sub-interfaces.
|
_Prover
An object realizing an instance of a prover.
|
_Strategy
The strategy defines the way the proof-search space is visited; at every
iteration the engine invokes
_Strategy.nextRule(_AbstractGoal, IterationInfo) ) to determine the rule to
apply to the current-goal of the proof-search. |
ProofSearchResult
The result of the proof-search.
|
ProvabilityStatus
The status of an input formula.
|
ProverName
Utility class to manage the name of a prover.
|
Trace
A trace describes the steps performed during a proof search; it provides data
about:
the prover used to generate the proof-search;
the initial node-set of the proof-search;
the status of the proof-search;
the root of the trace-tree describing the performed proof search.
We call trace tree the tree describing the proof-search.
|
TraceNode
A node in the proof-trace, it describes a rule applied in the proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
Class and Description |
---|
_AbstractFormula
Represents a formula during proof-search.
|
_AbstractGoal
An abstract goal represent a goal during proof-search.
|