See: Description
Interface | 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.
|
_BranchExistsRule |
This interface describes a branch-exists rule, namely a backtrack rule that
succeeds if at least one of its subgoals succeeds.
|
_ClashDetectionRule |
An object realizing a clash-detection rule.
|
_MetaBacktrackRule |
A meta-backtrack rule specifies an enumeration of backtrack
rules to try in the proof-search.
|
_OnRuleCompletedListener |
Specifies that the rule implementing this interface listens for the
on-rule-completed event.
|
_OnRuleResumedListener |
Specifies that the rule implementing this interface listens for the
on-resume-event.
|
_Prover |
An object realizing an instance of a prover.
|
_RegularRule |
A regular rule is a rule generating one or more sub-goals to solve.
|
_RuleWithDetails |
Provides some details about the rule; the method
_RuleWithDetails.getDetails() is
invoked by the engine when it works in verbose mode to provide some extra
information about the rule application implementing this interface. |
_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. |
Class | Description |
---|---|
Engine |
The engine performs a depth-first search of a derivation tree.
|
ForceBranchFailure |
This rule force branch failure.
|
ForceBranchSuccess |
An final instance of
_ClashDetectionRule whose
_ClashDetectionRule.status() always returns
ProofSearchResult.SUCCESS . |
IterationInfo |
A bunch of data describing the last iteration performed by the engine.
|
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.
|
Enum | Description |
---|---|
Engine.ExecutionMode |
Engine execution mode flags.
|
IterationInfo.Move |
The possible moves performed by the engine.
|
ProofSearchResult |
The result of the proof-search.
|
ProvabilityStatus |
The status of an input formula.
|
RuleType |
The type of a rule classify a rule applied during proof search.
|
Exception | Description |
---|---|
EngineException |
An error occurring during an engine execution.
|
NoSuchBacktrackRuleException |
Specialised version of
NoSuchElementException thrown by the
_MetaBacktrackRule.nextRule() method to indicate that there are no
more backtrack rules. |
NoSuchSubgoalException |
Specialised version of
NoSuchElementException thrown by the
_RegularRule.nextSubgoal() and
_BranchExistsRule.nextBranchExistsSubgoal() to to indicate that there
are no more subgoal returned by the rule. |
TraceException |
Thrown if something goes wrong managing a trace.
|