Uses of Class
de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderExistentialQuantification

Packages that use SecondOrderExistentialQuantification

de.uni_tuebingen.sfb.lichtenstein.binarytrees
de.uni_tuebingen.sfb.lichtenstein.formulas

Uses of SecondOrderExistentialQuantification in de.uni_tuebingen.sfb.lichtenstein.binarytrees

Methods in de.uni_tuebingen.sfb.lichtenstein.binarytrees with parameters of type SecondOrderExistentialQuantification

protected void

MonaFormulaBuilder.visit(SecondOrderExistentialQuantification form) Visit an existential quantification.

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

Methods in de.uni_tuebingen.sfb.lichtenstein.formulas that return SecondOrderExistentialQuantification

SecondOrderExistentialQuantification	SecondOrderVariable.exists(Formula form) Returns the existential quantification of the given formula over this variable.
SecondOrderExistentialQuantification	Formula.exists(SecondOrderVariable var) Return the existential quantification of this formula over the given first order variable.
SecondOrderExistentialQuantification	FormulaImpl.exists(SecondOrderVariable var) Return the existential quantification of this formula over the given first order variable.
static SecondOrderExistentialQuantification	Formulas.exists(SecondOrderVariable var, Formula form) Return the existential quantification of the given formula over the given first order variable.
SecondOrderExistentialQuantification	SecondOrderExistentialQuantification.getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.

Methods in de.uni_tuebingen.sfb.lichtenstein.formulas with parameters of type SecondOrderExistentialQuantification

protected abstract void

FormulaVisitor.visit(SecondOrderExistentialQuantification form) Visit an existential quantification.