de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderExistentialQuantification

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderQuantor
              de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderExistentialQuantification

All Implemented Interfaces:

Formula, Quantification, Visitable, Serializable

public final class FirstOrderExistentialQuantification
extends FirstOrderQuantor

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

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

FirstOrderExistentialQuantification(FirstOrderVariable 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.
FirstOrderExistentialQuantification	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.FirstOrderQuantor

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

FirstOrderExistentialQuantification

public FirstOrderExistentialQuantification(FirstOrderVariable 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 FirstOrderExistentialQuantification 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.