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 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

containsVariable, equals, getArgument, getBoundVariable, getFirstIndexOf, getNbBoundVariables, getNbFreeVariables, getNbSubformulas, getNbVariables, getPredicates, getSubformulaAt, getVariableAt, hashCode, isFreeVariable, 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, getFreeVariables, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

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

and, exists, exists, forAll, forAll, getFreeVariables, 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)

Postcondition:

The bound variable is set to the given variable.

| new.getBoundVariable() == var

Postcondition:

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 de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException

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

Specified by:

accept in interface Visitable

Overrides:

accept in class FormulaImpl

Parameters:

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

Throws:

VisitorException

A visitor can throw an exception.