Package | Description |
---|---|
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.
|
Modifier and Type | Class and Description |
---|---|
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 | Method and Description |
---|---|
BTModalFormula |
BTModalFormulaFactory.buildAtomic(java.lang.String name) |
BTModalFormula |
BTModalFormulaFactory.buildCompound(ModalConnective mainConnective,
BTModalFormula... subformulas) |
BTModalFormula |
BTModalFormulaFactory.buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree) |
BTModalFormula |
BTModalFormulaProposition.convertToCNF() |
BTModalFormula |
BTModalFormulaCompound.convertToCNF() |
abstract BTModalFormula |
BTModalFormula.convertToCNF() |
BTModalFormula[] |
BTModalFormulaProposition.immediateSubformulas() |
BTModalFormula[] |
BTModalFormulaCompound.immediateSubformulas() |
abstract BTModalFormula[] |
BTModalFormula.immediateSubformulas() |
Modifier and Type | Method and Description |
---|---|
BTModalFormula |
BTModalFormulaFactory.buildCompound(ModalConnective mainConnective,
BTModalFormula... subformulas) |
Constructor and Description |
---|
BTModalFormulaCompound(ModalConnective mainConnective,
BTModalFormula sub)
Build an instance of a compound formula with an unary main connective.
|
BTModalFormulaCompound(ModalConnective mainConnective,
BTModalFormula left,
BTModalFormula right)
Build an instance of a compound formula with a binary main connective.
|
Modifier and Type | Method and Description |
---|---|
ModalFormula |
ModalFormulaFactory.buildFrom(BTModalFormula wff)
Build an instance of the specified
BTModalFormula . |