Uses of Interface
de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable

Packages that use Visitable

de.uni_tuebingen.sfb.lichtenstein.formulas

Uses of Visitable in de.uni_tuebingen.sfb.lichtenstein.formulas

Subinterfaces of Visitable in de.uni_tuebingen.sfb.lichtenstein.formulas

interface	Formula A class for specifying a formula in monadic second order logic.
interface	Quantification A class representing a quantification.

Classes in de.uni_tuebingen.sfb.lichtenstein.formulas that implement Visitable

class	AtomicFormula A class representing an atomic formula.
class	BinaryJunctor A superclass for implication and equivalence, implementing common methods for binary junctors.
class	ComposedFormula A class representing a composed formula, i.e. a formula which consists of other formulas, connected by an operator.
class	Conjunction A class representing the conjunction of formulas.
class	Disjunction A class representing the disjunction of formulas.
class	Dominance A class representing the atomic formula which says one node dominates another.
class	Equivalence A class representing the equivalence in logical formulas.
class	FirstOrderEquality A class representing the atomic formula that says two first order variables are equal.
class	FirstOrderExistentialQuantification A class representing the existential quantification of a formula over a first order variable.
class	FirstOrderQuantor A class for representing quantors on first order variables, implementing common methods for existential and universal quantors.
class	FirstOrderUniversalQuantification A class representing universal quantification of a formula over a first order variable.
class	FormulaImpl A class providing implementations of the formula interface where possible.
class	ImmediateDominance A class representing the atomic formula which says one node immediately dominates another.
class	ImmediatePrecedence A class representing the atomic formula which says one node immediately precedes another.
class	Implication A class representing the implication of formulas.
class	Inclusion A class representing inclusion of a first order variable in a set denotator.
class	NaryJunctor A superclass for conjunction and disjunction, implementing common methods for binary junctors.
class	Negation A class representing logical negation of a formula.
class	Precedence A class representing the atomic formula which says one node precedes another.
class	ProperDominance A class representing the atomic formula which says one node properly dominates another.
class	SecondOrderEquality A class representing the atomic formula that says two variables are equal.
class	SecondOrderExistentialQuantification A class representing the existential quantification of a formula over a second order variable.
class	SecondOrderQuantor A class for representing quantors on second order variables, implementing common methods for existential and universal quantors.
class	SecondOrderUniversalQuantification A class representing universal quantification of a formula over a second order variable.
class	Subset A class for representing the atomic formula which says a variable is a subset of another variable
class	UnaryJunctor A class representing a unary junctor, having one argument.