Package de.uni_tuebingen.sfb.lichtenstein.formulas

Interface Summary
Formula A class for specifying a formula in monadic second order logic.
Quantification A class representing a quantification.
Visitable An interface indicating a formula visitor can visit this class.
 

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.
 



© Copyright 2008 Hendrik Maryns   Creative Commons License