de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderUniversalQuantification

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderQuantor
              extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderUniversalQuantification
All Implemented Interfaces:
Formula, Quantification, Visitable, Serializable

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

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