See: Description
Interface | Description |
---|---|
_FormulaSet |
Interface for a set of formulas.
|
_Sequent |
Interface modeling a sequent of the form
S ==> T where
S and T are sets of propositional formulas. |
_SingleSuccedentSequent |
Interface modelling a sequent of the form
S ==> H where
S is a sets of propositional formulas and H is a
propositional formula. |
Class | Description |
---|---|
BitSetOfFormulas |
Sets of formulas implemented over bitsets.
|
Formula |
Formula of this package are realized by objects implementing this interface.
|
FormulaFactory |
The factory building formulas.
|
FormulaLatexFormatter |
Provides a static method to generate the LaTeX of a formula.
|
FormulaProposition |
An atomic propositional formula.
|
FormulaSetOnHashSet |
Set of signed formulas implemented over HashSet.
|
FormulaSetOnList |
Set of signed formulas implemented over LinkedList.
|
PropositionalSubstitution |
A propositional substitution is a mapping between propositional variables and
formulas.
|
SequentOnArray |
Implementation of the
_Sequent interface using an array of integers
to represents the sequent. |
SequentOnBitSet |
Implementation of the
_Sequent interface using an array of integers
to represents the sequent. |
SequentOnBSF |
Implementation of the
_Sequent interface using
BitSetOfFormulas to represent the left-hand and the right-hand sides. |
SequentOnBSFWithFormulasByType |
Implementation of the
_Sequent interface using
BitSetOfFormulas to represent the left-hand and the right-hand sides. |
SequentOnLists |
Implementation of the
_Sequent interface using lists to store left
and right formulas. |
SingleSuccedentSequentOnArray |
Implementation of the
_SingleSuccedentSequent interface using an
array of integers to represents the sequent. |
SingleSuccedentSequentOnBitSet | |
SingleSuccedentSequentOnBSF |
Implementation of the
_Sequent interface on Formula using a
BitSetOfFormulas to represent the left-hand side. |
SingleSuccedentSequentOnLists |
Implementation of the
_SingleSuccedentSequent interface using lists
to store left formulas. |
Substitution |
Exception | Description |
---|---|
ClosedFactoryException |
Formula
class and can be
generated by the methods of FormulaFactory
. This
factory provide an efficient implementation of formulas based on graphs which
avoid subformulas duplication. This means that multiple occurrences of the
same formula are identified.