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

Method Summary

Formula	getArgument() Returns the formula this quantor acts on.
Variable	getBoundVariable() Returns the variable that is bound by this quantor.

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula

and, containsVariable, exists, exists, forAll, forAll, getFreeVariables, getNormalForm, getPredicates, getVariables, iff, implies, isClosed, isFree, not, or

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable

accept

Method Detail

getBoundVariable

Variable getBoundVariable()

Returns the variable that is bound by this quantor.

Returns:

The bound variable.

getArgument

Formula getArgument()

Returns the formula this quantor acts on.

Returns:

This is the first subformula. | result == getSubfomulaAt(0)