Uses of Package
de.uni_tuebingen.sfb.lichtenstein.formulas

Classes in de.uni_tuebingen.sfb.lichtenstein.formulas used by de.uni_tuebingen.sfb.lichtenstein.formulas

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.

Formula
A class for specifying a formula in monadic second order logic.

FormulaImpl
A class providing implementations of the formula interface where possible.

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.

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.

Quantification
A class representing a quantification.

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.

Visitable
An interface indicating a formula visitor can visit this class.