de.uni_tuebingen.sfb.lichtenstein.formulas
Interface Quantification
- All Superinterfaces:
- Formula, Serializable, Visitable
- All Known Implementing Classes:
- FirstOrderExistentialQuantification, FirstOrderQuantor, FirstOrderUniversalQuantification, SecondOrderExistentialQuantification, SecondOrderQuantor, SecondOrderUniversalQuantification
public interface Quantification
- extends Formula
A class representing a quantification. This can be implemented in a various number of ways, including working on
first and second order variables, existential and universal quantification. TODO: possibility for more variables
- Author:
- Hendrik Maryns
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula |
and, containsVariable, exists, exists, forAll, forAll, getFirstIndexOf, getFreeVariables, getNbBoundVariables, getNbFreeVariables, getNbVariables, getNormalForm, getPredicates, getVariableAt, getVariables, iff, implies, isClosed, isFreeVariable, not, or |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable |
accept |
getBoundVariable
Variable getBoundVariable()
- Returns the variable that is bound by this quantor.
The bound variable.
getArgument
Formula getArgument()
- Returns the formula this quantor acts on.
This is the first subformula.
| result == getSubfomulaAt(0)