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. |
ImmediatePrecedence |
A class representing the atomic formula which says one node immediately precedes 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. |