Package | Description |
---|---|
jtabwb.engine |
Main classes implementing the engine; it specifies the interfaces with the
user defined prover.
|
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.
|
Modifier and Type | Method and Description |
---|---|
_AbstractFormula |
_RegularRule.mainFormula()
Returns the main formula of this rule or
null if this rule
does not have a main formula. |
_AbstractFormula |
_BranchExistsRule.mainFormula()
The main formula of this rule or
null if this rule does not
have a main formula. |
Modifier and Type | Method and Description |
---|---|
_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 |
_ModalFormula
Interface describing modal formulas on the set of connectives
ModalConnective . |
Modifier and Type | Class and Description |
---|---|
class |
BTModalFormula
The root class for parsed formulas implementation.
|
class |
BTModalFormulaCompound
An instance of this class models a compound propositional formula.
|
class |
BTModalFormulaProposition
An instance of this class models an atomic formula (a proposition).
|
Modifier and Type | Class and Description |
---|---|
class |
ModalFormula
A modal formula.
|
class |
ModalFormulaProposition
An propositional variable.
|
Modifier and Type | Interface and Description |
---|---|
interface |
_PropositionalFormula
Interface describing propositional formulas on the set of connecetives
PropositionalConnective . |
Modifier and Type | Class and Description |
---|---|
class |
BTFormula
A simple implementation of a formula as a binary tree.
|
class |
BTFormulaCompound
Implementation of a propositional compound formula, that is a formula
obtained by combining sub-formulas by means of a propositional connective.
|
class |
BTFormulaProposition
Implementation of a propositional variable (an atomic formula).
|
Modifier and Type | Class and Description |
---|---|
class |
Formula
Formula of this package are realized by objects implementing this interface.
|
class |
FormulaProposition
An atomic propositional formula.
|