de.uni_tuebingen.sfb.lichtenstein.formulas
Class SecondOrderExistentialQuantification

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderQuantor
              de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderExistentialQuantification

All Implemented Interfaces:

Formula, Quantification, Visitable, Serializable

public final class SecondOrderExistentialQuantification
extends SecondOrderQuantor

A class representing the existential quantification of a formula over a second order variable.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

SecondOrderExistentialQuantification(SecondOrderVariable var, Formula arg)
Initialize a new existential quantor, given a variable to bind and a formula to act upon.

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
SecondOrderExistentialQuantification	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
String	getSymbol() Return the textual representation of this binary junctor.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderQuantor

computePredicates, computeVariables, containsVariable, equals, getArgument, getBoundVariable, getFreeVariables, getNbSubformulas, getSubformulaAt, hashCode, isFree, toString

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula

getAllSubformulas

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl

and, exists, exists, forAll, forAll, getPredicates, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

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

and, exists, exists, forAll, forAll, getPredicates, getVariables, iff, implies, isClosed, not, or

Constructor Detail

SecondOrderExistentialQuantification

public SecondOrderExistentialQuantification(SecondOrderVariable var,
                                            Formula arg)

Initialize a new existential quantor, given a variable to bind and a formula to act upon.

Parameters:

var - The variable that is bound by this quantor.

arg - The formula which this quantor acts upon.

Precondition:

The given variable and formula must be effective and the variable must not be bound in the given formula. | var != null && arg != null && arg.isFreeVariable(var)

Postconditions:

The bound variable is set to the given variable. | new.getBoundVariable() == var

The formula on which this quantor acts is set to the given formula. | new.getArgument() == arg

Method Detail

getNormalForm

public SecondOrderExistentialQuantification getNormalForm()

Get a normal form with only conjunction, disjunction, negation and existential quantification.

Returns:

The existential quantification of the normal form of the argument formula, over the same variable. | result == getArgument().getNormalForm().exists(getBoundVariable())

getSymbol

public String getSymbol()

Return the textual representation of this binary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol THERE EXISTS: ∃. | result == "∃"

accept

public void accept(FormulaVisitor visitor)
            throws VisitorException

Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.

Parameters:

visitor - The visitor that is to be accepted to do its work.

Throws:

VisitorException - [CAN] A visitor can throw an exception.