de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderUniversalQuantification

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

All Implemented Interfaces:

Formula, Quantification, Visitable, Serializable

public final class FirstOrderUniversalQuantification
extends FirstOrderQuantor

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

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

FirstOrderUniversalQuantification(FirstOrderVariable var, Formula arg)
Initialize a new universal quantor, given a variable to bind and a formula to act upon.

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
Formula	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

FirstOrderUniversalQuantification

public FirstOrderUniversalQuantification(FirstOrderVariable var,
                                         Formula arg)

Initialize a new universal 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 Formula getNormalForm()

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

Returns:

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

getSymbol

public String getSymbol()

Return the textual representation of this binary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol FOR ALL: ∀. | 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.