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.prop.formula |
An implementation of propositional formulas based on graphs.
|
Modifier and Type | Method and Description |
---|---|
_AbstractGoal |
_AbstractGoal.clone()
Returns a fresh copy of this goal
|
_AbstractGoal |
Engine.getInitialGoal()
Returns the initial goal.
|
_AbstractGoal |
Trace.getInitialNodeSet()
Returns the initial node set (the node set at the root of the
proof-search).
|
_AbstractGoal |
TraceNode.getPremise() |
_AbstractGoal |
ForceBranchFailure.goal()
Returns the abstract node set on which the the proof-search failed.
|
_AbstractGoal |
_MetaBacktrackRule.goal()
Returns the goal of this meta-backtrack rule application.
|
_AbstractGoal |
_ClashDetectionRule.goal()
Returns the goal on which this this clash-detection rule act.
|
_AbstractGoal |
_BranchExistsRule.nextBranchExistsSubgoal()
Returns the next subgoal of this rule.
|
_AbstractGoal |
_RegularRule.nextSubgoal()
Returns the next subgoal of this rule.
|
_AbstractGoal |
ForceBranchSuccess.premise()
Returns the abstract node set on which the the proof-search failed.
|
Modifier and Type | Method and Description |
---|---|
_AbstractRule |
_Strategy.nextRule(_AbstractGoal currentGoal,
IterationInfo lastIteration)
This is a call-back method invoked by the engine when it needs to determine
the rule to to apply to
currentGoal ; doing this the engine
provides to the method as second argument a bunch of data describing the
last performed iteration. |
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.
|
ForceBranchFailure(java.lang.String name,
_AbstractGoal goal) |
ForceBranchSuccess(java.lang.String name,
_AbstractGoal goal) |
Modifier and Type | Method and Description |
---|---|
_AbstractGoal |
_InitialGoalBuilder.buildInitialNodeSet(ProblemDescription inputProblem)
Build a goal from the specified problem description.
|
_AbstractGoal |
ProofSearchData.goal()
Returns the goal of the proof-search.
|
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) . |
Modifier and Type | Method and Description |
---|---|
_AbstractGoal |
CTreeNode.getNodeSet() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
_LatexCTreeFormatter.format(_AbstractGoal node)
Returns the LaTeX translation of the spcified node set.
|
_AbstractRule |
_TraceManager.getRuleByName(java.lang.String name,
_AbstractGoal premise,
_AbstractFormula mainFormula)
Returns the instance of the rule with the specified name applied to the
specified arguments.
|
Modifier and Type | Interface and Description |
---|---|
interface |
_Sequent
Interface modeling a sequent of the form
S ==> T where
S and T are sets of propositional formulas. |
interface |
_SingleSuccedentSequent
Interface modelling a sequent of the form
S ==> H where
S is a sets of propositional formulas and H is a
propositional formula. |
Modifier and Type | Class and Description |
---|---|
class |
SequentOnArray
Implementation of the
_Sequent interface using an array of integers
to represents the sequent. |
class |
SequentOnBitSet
Implementation of the
_Sequent interface using an array of integers
to represents the sequent. |
class |
SequentOnBSF
Implementation of the
_Sequent interface using
BitSetOfFormulas to represent the left-hand and the right-hand sides. |
class |
SequentOnBSFWithFormulasByType
Implementation of the
_Sequent interface using
BitSetOfFormulas to represent the left-hand and the right-hand sides. |
class |
SequentOnLists
Implementation of the
_Sequent interface using lists to store left
and right formulas. |
class |
SingleSuccedentSequentOnArray
Implementation of the
_SingleSuccedentSequent interface using an
array of integers to represents the sequent. |
class |
SingleSuccedentSequentOnBitSet
|
class |
SingleSuccedentSequentOnBSF
Implementation of the
_Sequent interface on Formula using a
BitSetOfFormulas to represent the left-hand side. |
class |
SingleSuccedentSequentOnLists
Implementation of the
_SingleSuccedentSequent interface using lists
to store left formulas. |