Package | Description |
---|---|
jtabwbx.prop.formula |
An implementation of propositional formulas based on graphs.
|
Modifier and Type | Class and Description |
---|---|
class |
FormulaProposition
An atomic propositional formula.
|
Modifier and Type | Method and Description |
---|---|
Formula |
FormulaProposition.applyIntuitionisticPartialSubstitution(Substitution subst) |
abstract Formula |
Formula.applyIntuitionisticPartialSubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution as
intuitionistic partial substitution.
|
Formula |
FormulaProposition.applySubstitution(PropositionalSubstitution subst) |
abstract Formula |
Formula.applySubstitution(PropositionalSubstitution subst)
Returns the formula obtained by applying the specified substitution on
propositional formulas.
|
Formula |
FormulaProposition.applySubstitution(Substitution subst) |
abstract Formula |
Formula.applySubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution.
|
Formula |
FormulaFactory.buildCompound(PropositionalConnective mainConnective,
Formula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
Formula |
FormulaFactory.buildFrom(BTFormula wff)
Build an instance of the specified
BTFormula . |
Formula |
FormulaFactory.buildFrom(Formula wff)
Build an instance of the specified formula in this factory.
|
Formula |
FormulaFactory.buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
Build a formula from the specified parse-tree.
|
Formula |
FormulaProposition.calculateBooleanSimplification() |
abstract Formula |
Formula.calculateBooleanSimplification()
Returns the formula obtained by applying boolean simplifications on this
formula.
|
Formula |
FormulaFactory.getByIndex(int index) |
Formula |
FormulaSetOnList.getFirst() |
Formula |
FormulaSetOnHashSet.getFirst() |
Formula |
BitSetOfFormulas.getFirst() |
Formula |
_FormulaSet.getFirst()
Returns the first formula in this set or
null if this set is
empty. |
Formula |
BitSetOfFormulas.getFirst(FormulaType type) |
Formula |
BitSetOfFormulas.getFirstAndRemove()
Returns the first formula of this bitset and remove it from the bitset.
|
Formula |
BitSetOfFormulas.getFirstAndRemove(FormulaType type)
Returns the first formula with the specified type of this bitset and remove
it from the bitset.
|
Formula |
SingleSuccedentSequentOnLists.getLeft() |
Formula |
SingleSuccedentSequentOnBSF.getLeft() |
Formula |
SingleSuccedentSequentOnBitSet.getLeft() |
Formula |
SingleSuccedentSequentOnArray.getLeft() |
Formula |
_SingleSuccedentSequent.getLeft()
Returns a formula from the left hand side of the sequent or
null if le theft hand side is empty. |
Formula |
SingleSuccedentSequentOnLists.getLeft(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnBSF.getLeft(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnBitSet.getLeft(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnArray.getLeft(FormulaType formulaType) |
Formula |
SequentOnLists.getLeft(FormulaType formulaType) |
Formula |
SequentOnBSFWithFormulasByType.getLeft(FormulaType formulaType) |
Formula |
SequentOnBSF.getLeft(FormulaType formulaType) |
Formula |
SequentOnBitSet.getLeft(FormulaType formulaType) |
Formula |
SequentOnArray.getLeft(FormulaType formulaType) |
Formula |
_SingleSuccedentSequent.getLeft(FormulaType formulaType)
Returns a formula of the specified type contained in the left hand side of
the sequent or
null if no formula of the specified type occurs
in this sequent. |
Formula |
_Sequent.getLeft(FormulaType formulaType)
Returns a formula of the specified type contained in the left hand side of
the sequent or
null if no formula of the specified type occurs
in this sequent. |
Formula |
SingleSuccedentSequentOnLists.getRight() |
Formula |
SingleSuccedentSequentOnBSF.getRight() |
Formula |
SingleSuccedentSequentOnBitSet.getRight() |
Formula |
SingleSuccedentSequentOnArray.getRight() |
Formula |
_SingleSuccedentSequent.getRight()
Returns the formula in the right hand side of this sequent or
null if the right hand side of this sequent is empty. |
Formula |
SequentOnLists.getRight(FormulaType formulaType) |
Formula |
SequentOnBSFWithFormulasByType.getRight(FormulaType formulaType) |
Formula |
SequentOnBSF.getRight(FormulaType formulaType) |
Formula |
SequentOnBitSet.getRight(FormulaType formulaType) |
Formula |
SequentOnArray.getRight(FormulaType formulaType) |
Formula |
_Sequent.getRight(FormulaType formulaType)
Returns the formula in the right hand side of this sequent or
null if the formula in the right hand side does not have the
specified type. |
Formula |
SingleSuccedentSequentOnLists.getRightFormulaOfType(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnBSF.getRightFormulaOfType(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnBitSet.getRightFormulaOfType(FormulaType formulaType) |
Formula |
SingleSuccedentSequentOnArray.getRightFormulaOfType(FormulaType formulaType) |
Formula |
_SingleSuccedentSequent.getRightFormulaOfType(FormulaType formulaType)
Returns the formula in the right hand side of this sequent if the formula
has the specified type or
null if the formula in the right
hand side does not have the specified type. |
Formula[] |
FormulaProposition.immediateSubformulas() |
abstract Formula[] |
Formula.immediateSubformulas()
The subformulas of this formula.
|
Formula[] |
FormulaSetOnList.toArray() |
Formula[] |
FormulaSetOnHashSet.toArray() |
Formula[] |
BitSetOfFormulas.toArray() |
Formula[] |
_FormulaSet.toArray()
Returns an array of formulas containing all of the formulas in this set.
|
Modifier and Type | Method and Description |
---|---|
java.util.ArrayList<Formula> |
FormulaFactory.generatedFormulas()
Returns a copy of the list of formulas generated by this factory.
|
java.util.Collection<Formula> |
FormulaSetOnList.getAllFormulas() |
java.util.Collection<Formula> |
FormulaSetOnHashSet.getAllFormulas() |
java.util.Collection<Formula> |
BitSetOfFormulas.getAllFormulas()
Returns the collection containing all the formulas in this set or null if
this set is empty.
|
java.util.Collection<Formula> |
_FormulaSet.getAllFormulas()
Returns a collection containing all the formulas in this set or
null if this set is empty. |
java.util.Collection<Formula> |
BitSetOfFormulas.getAllFormulas(FormulaType formulaType)
Returns a collection containing all formulas with the specified formula
type in this set or null if this set does not contain any formulas with the
specified formula type.
|
java.util.Collection<Formula> |
SingleSuccedentSequentOnLists.getAllLeftFormulas() |
java.util.Collection<Formula> |
SingleSuccedentSequentOnBSF.getAllLeftFormulas() |
java.util.Collection<Formula> |
SingleSuccedentSequentOnBitSet.getAllLeftFormulas() |
java.util.Collection<Formula> |
SingleSuccedentSequentOnArray.getAllLeftFormulas() |
java.util.Collection<Formula> |
_SingleSuccedentSequent.getAllLeftFormulas()
Returns the set containg all the formulas in the left hand side of this
sequent or
null if the left hand side of this sequent is
empty. |
java.util.Collection<Formula> |
SingleSuccedentSequentOnLists.getAllLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SingleSuccedentSequentOnBSF.getAllLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SingleSuccedentSequentOnBitSet.getAllLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SingleSuccedentSequentOnArray.getAllLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
_SingleSuccedentSequent.getAllLeftFormulas(FormulaType formulaType)
Returns the collection of all the formulas in the left hand side of this
sequent with the specified type or
null if the left hand side
of this sequent does not contain any formula of the specified type. |
java.util.Collection<Formula> |
SequentOnLists.getLeftFormulas() |
java.util.Collection<Formula> |
SequentOnBSFWithFormulasByType.getLeftFormulas() |
java.util.Collection<Formula> |
SequentOnBSF.getLeftFormulas() |
java.util.Collection<Formula> |
SequentOnBitSet.getLeftFormulas() |
java.util.Collection<Formula> |
SequentOnArray.getLeftFormulas() |
java.util.Collection<Formula> |
_Sequent.getLeftFormulas()
Returns the set containg all the formulas in the left hand side of this
sequent or
null if the left hand side of this sequent is
empty. |
java.util.Collection<Formula> |
SequentOnLists.getLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBSFWithFormulasByType.getLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBSF.getLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBitSet.getLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnArray.getLeftFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
_Sequent.getLeftFormulas(FormulaType formulaType)
Returns the collection of all the formulas in the left hand side of this
sequent with the specified type or
null if the left hand side
of this sequent does not contain any formula of the specified type. |
java.util.Collection<Formula> |
SequentOnLists.getRightFormulas() |
java.util.Collection<Formula> |
SequentOnBSFWithFormulasByType.getRightFormulas() |
java.util.Collection<Formula> |
SequentOnBSF.getRightFormulas() |
java.util.Collection<Formula> |
SequentOnBitSet.getRightFormulas() |
java.util.Collection<Formula> |
SequentOnArray.getRightFormulas() |
java.util.Collection<Formula> |
_Sequent.getRightFormulas()
Returns the set containg all the formulas in the right hand side of this
sequent or
null if the right hand side of this sequent is
empty. |
java.util.Collection<Formula> |
SequentOnLists.getRightFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBSFWithFormulasByType.getRightFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBSF.getRightFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnBitSet.getRightFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
SequentOnArray.getRightFormulas(FormulaType formulaType) |
java.util.Collection<Formula> |
_Sequent.getRightFormulas(FormulaType formulaType)
Returns the collection of all the formulas in the right hand side of this
sequent with the specified type or
null if the right hand side
of this sequent does not contain any formula of the specified type. |
java.util.Iterator<Formula> |
FormulaSetOnHashSet.iterator() |
java.util.Iterator<Formula> |
BitSetOfFormulas.iterator() |
java.util.Iterator<Formula> |
_FormulaSet.iterator()
Returns an iterator over the formulas in this set.
|
java.util.Iterator<Formula> |
SequentOnLists.leftSideIterator() |
java.util.Iterator<Formula> |
SequentOnBSFWithFormulasByType.leftSideIterator() |
java.util.Iterator<Formula> |
SequentOnBSF.leftSideIterator() |
java.util.Iterator<Formula> |
SequentOnBitSet.leftSideIterator() |
java.util.Iterator<Formula> |
SequentOnArray.leftSideIterator() |
java.util.Iterator<Formula> |
_Sequent.leftSideIterator() |
java.util.Iterator<Formula> |
SequentOnLists.rigtSideIterator() |
java.util.Iterator<Formula> |
SequentOnBSFWithFormulasByType.rigtSideIterator() |
java.util.Iterator<Formula> |
SequentOnBSF.rigtSideIterator() |
java.util.Iterator<Formula> |
SequentOnBitSet.rigtSideIterator() |
java.util.Iterator<Formula> |
SequentOnArray.rigtSideIterator() |
java.util.Iterator<Formula> |
_Sequent.rigtSideIterator() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
FormulaLatexFormatter._toLatex(Formula wff,
boolean parenthesize) |
boolean |
FormulaSetOnHashSet.add(Formula swff) |
boolean |
BitSetOfFormulas.add(Formula wff) |
boolean |
_FormulaSet.add(Formula wff)
Add the specified formula to this set and returns
true if this
set did not already contain the specified formula. |
void |
SingleSuccedentSequentOnLists.addLeft(Formula wff) |
void |
SingleSuccedentSequentOnBSF.addLeft(Formula wff) |
void |
SingleSuccedentSequentOnBitSet.addLeft(Formula wff) |
void |
SingleSuccedentSequentOnArray.addLeft(Formula wff) |
void |
SequentOnLists.addLeft(Formula wff) |
void |
SequentOnBSFWithFormulasByType.addLeft(Formula wff) |
void |
SequentOnBSF.addLeft(Formula wff) |
void |
SequentOnBitSet.addLeft(Formula wff) |
void |
SequentOnArray.addLeft(Formula wff) |
void |
_SingleSuccedentSequent.addLeft(Formula wff)
Add the specified formula to the left hand side of this sequent.
|
void |
_Sequent.addLeft(Formula wff)
Add the specified formula to the left hand side of this sequent.
|
void |
SingleSuccedentSequentOnLists.addRight(Formula wff) |
void |
SingleSuccedentSequentOnBSF.addRight(Formula wff) |
void |
SingleSuccedentSequentOnBitSet.addRight(Formula wff) |
void |
SingleSuccedentSequentOnArray.addRight(Formula wff) |
void |
SequentOnLists.addRight(Formula wff) |
void |
SequentOnBSFWithFormulasByType.addRight(Formula wff) |
void |
SequentOnBSF.addRight(Formula wff) |
void |
SequentOnBitSet.addRight(Formula wff) |
void |
SequentOnArray.addRight(Formula wff) |
void |
_SingleSuccedentSequent.addRight(Formula wff)
This method add the specified formula in the right hand side of this
sequent.
|
void |
_Sequent.addRight(Formula wff)
This method add the specified formula in the right hand side of this
sequent.
|
static SingleSuccedentSequentOnBitSet |
SingleSuccedentSequentOnBitSet.buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
static SingleSuccedentSequentOnArray |
SingleSuccedentSequentOnArray.buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
Formula |
FormulaFactory.buildCompound(PropositionalConnective mainConnective,
Formula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
Formula |
FormulaFactory.buildFrom(Formula wff)
Build an instance of the specified formula in this factory.
|
boolean |
FormulaSetOnList.contains(Formula swff) |
boolean |
FormulaSetOnHashSet.contains(Formula swff) |
boolean |
BitSetOfFormulas.contains(Formula wff) |
boolean |
_FormulaSet.contains(Formula swff)
Returns
true if and only if this set contains the specified
formula. |
boolean |
SingleSuccedentSequentOnLists.containsLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnBSF.containsLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnBitSet.containsLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnArray.containsLeft(Formula wff) |
boolean |
SequentOnLists.containsLeft(Formula wff) |
boolean |
SequentOnBSFWithFormulasByType.containsLeft(Formula wff) |
boolean |
SequentOnBSF.containsLeft(Formula wff) |
boolean |
SequentOnBitSet.containsLeft(Formula wff) |
boolean |
SequentOnArray.containsLeft(Formula wff) |
boolean |
_SingleSuccedentSequent.containsLeft(Formula wff)
Returns
true if this sequent contains the specified formula in
the left hand side and false otherwise. |
boolean |
_Sequent.containsLeft(Formula wff)
Returns
true if this sequent contains the specified formula in
the left hand side and false otherwise. |
boolean |
SequentOnLists.containsRight(Formula wff) |
boolean |
SequentOnBSFWithFormulasByType.containsRight(Formula wff) |
boolean |
SequentOnBSF.containsRight(Formula wff) |
boolean |
SequentOnBitSet.containsRight(Formula wff) |
boolean |
SequentOnArray.containsRight(Formula wff) |
boolean |
_Sequent.containsRight(Formula wff)
Returns
true if this sequent contains the specified formula in
the right hand side and false otherwise. |
boolean |
FormulaSetOnList.remove(Formula wff) |
boolean |
FormulaSetOnHashSet.remove(Formula wff) |
boolean |
BitSetOfFormulas.remove(Formula wff) |
boolean |
_FormulaSet.remove(Formula wff)
Returns the specified formula from this set.
|
boolean |
SingleSuccedentSequentOnLists.removeLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnBSF.removeLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnBitSet.removeLeft(Formula wff) |
boolean |
SingleSuccedentSequentOnArray.removeLeft(Formula wff) |
boolean |
SequentOnLists.removeLeft(Formula wff) |
boolean |
SequentOnBSFWithFormulasByType.removeLeft(Formula wff) |
boolean |
SequentOnBSF.removeLeft(Formula wff) |
boolean |
SequentOnBitSet.removeLeft(Formula wff) |
boolean |
SequentOnArray.removeLeft(Formula wff) |
boolean |
_SingleSuccedentSequent.removeLeft(Formula wff)
Removes the specified formula from the left hand side of this sequent, if
it is present.
|
boolean |
_Sequent.removeLeft(Formula wff)
Removes the specified formula from the left hand side of this sequent, if
it is present.
|
boolean |
SequentOnLists.removeRight(Formula wff) |
boolean |
SequentOnBSFWithFormulasByType.removeRight(Formula wff) |
boolean |
SequentOnBSF.removeRight(Formula wff) |
boolean |
SequentOnBitSet.removeRight(Formula wff) |
boolean |
SequentOnArray.removeRight(Formula wff) |
boolean |
_Sequent.removeRight(Formula wff)
Removes the right formula form this sequent.
|
java.lang.String |
FormulaLatexFormatter.toLatex(Formula wff)
Returns the LaTex source of the specified formula, the result of this
method must placed in math mode.
|
java.lang.String |
FormulaLatexFormatter.toLatex(Formula[] formulas,
java.lang.String separator)
Returns the LaTex source of the formulas in the given array; formulas are
separated by the specified separator.
|
Modifier and Type | Method and Description |
---|---|
void |
SequentOnLists.addLeft(java.util.Collection<Formula> formulas) |
void |
SequentOnBSFWithFormulasByType.addLeft(java.util.Collection<Formula> formulas) |
void |
SequentOnBSF.addLeft(java.util.Collection<Formula> formulas) |
void |
SequentOnBitSet.addLeft(java.util.Collection<Formula> formulas) |
void |
SequentOnArray.addLeft(java.util.Collection<Formula> formulas) |
void |
_Sequent.addLeft(java.util.Collection<Formula> formulas) |
void |
SequentOnLists.addRight(java.util.Collection<Formula> formulas) |
void |
SequentOnBSFWithFormulasByType.addRight(java.util.Collection<Formula> formulas) |
void |
SequentOnBSF.addRight(java.util.Collection<Formula> formulas) |
void |
SequentOnBitSet.addRight(java.util.Collection<Formula> formulas) |
void |
SequentOnArray.addRight(java.util.Collection<Formula> formulas) |
void |
_Sequent.addRight(java.util.Collection<Formula> formulas) |
static SingleSuccedentSequentOnBitSet |
SingleSuccedentSequentOnBitSet.buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
static SingleSuccedentSequentOnArray |
SingleSuccedentSequentOnArray.buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
java.lang.String |
FormulaLatexFormatter.toLatex(java.util.Collection<Formula> formulas,
java.lang.String separator)
Returns the LaTex source of the formulas in the given collection; formulas
are separated by the specified separator.
|