|
Class Summary |
| AtomicFormula |
A class representing an atomic formula. |
| BinaryJunctor |
A superclass for implication and equivalence, implementing common methods for binary junctors. |
| ComposedFormula |
A class representing a composed formula, i.e. a formula which consists of other formulas, connected by an operator. |
| Conjunction |
A class representing the conjunction of formulas. |
| Disjunction |
A class representing the disjunction of formulas. |
| Dominance |
A class representing the atomic formula which says one node dominates another. |
| Equivalence |
A class representing the equivalence in logical formulas. |
| FirstOrderEquality |
A class representing the atomic formula that says two first order variables are equal. |
| FirstOrderExistentialQuantification |
A class representing the existential quantification of a formula over a first order variable. |
| FirstOrderQuantor |
A class for representing quantors on first order variables, implementing common methods for existential and universal
quantors. |
| FirstOrderUniversalQuantification |
A class representing universal quantification of a formula over a first order variable. |
| FirstOrderVariable |
A class representing first order variables in the monadic second order logic. |
| FormulaImpl |
A class providing implementations of the formula interface where possible. |
| Formulas |
A class containing convenience methods to create formulas. |
| FormulaTemplate |
A class that represents a template for a formula, in which certain free variables still have to be filled in to get a
real formula. |
| FormulaVisitor |
A general interface representing a visitor that visits formulas. |
| ImmediateDominance |
A class representing the atomic formula which says one node immediately dominates another. |
| Implication |
A class representing the implication of formulas. |
| Inclusion |
A class representing inclusion of a first order variable in a set denotator. |
| NaryJunctor |
A superclass for conjunction and disjunction, implementing common methods for binary junctors. |
| Negation |
A class representing logical negation of a formula. |
| Precedence |
A class representing the atomic formula which says one node precedes another. |
| Predicate |
A class representing a predicate. |
| ProperDominance |
A class representing the atomic formula which says one node properly dominates another. |
| SecondOrderEquality |
A class representing the atomic formula that says two variables are equal. |
| SecondOrderExistentialQuantification |
A class representing the existential quantification of a formula over a second order variable. |
| SecondOrderQuantor |
A class for representing quantors on second order variables, implementing common methods for existential and
universal quantors. |
| SecondOrderUniversalQuantification |
A class representing universal quantification of a formula over a second order variable. |
| SecondOrderVariable |
A class representing second order variables in the monadic second order logic. |
| SetDenotator |
An abstract superclass for second order variables and predicates, both denotating sets of nodes. |
| Subset |
A class for representing the atomic formula which says a variable is a subset of another variable |
| UnaryJunctor |
A class representing a unary junctor, having one argument. |
| Variable |
A class representing variables and predicates in the monadic second order logic. |