de.uni_tuebingen.sfb.lichtenstein.formulas
Class SecondOrderVariable

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.SetDenotator
          extended by de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderVariable
All Implemented Interfaces:
Serializable

public class SecondOrderVariable
extends SetDenotator

A class representing second order variables in the monadic second order logic.

Author:
Hendrik Maryns
See Also:
Serialized Form

Constructor Summary
SecondOrderVariable()
          Initialize a new second order variable.
SecondOrderVariable(String name)
          Initialize a new second order variable with the given name.
 
Method Summary
 SecondOrderExistentialQuantification exists(Formula form)
          Returns the existential quantification of the given formula over this variable.
 SecondOrderUniversalQuantification forAll(Formula form)
          Returns the universal quantification of the given formula over this variable.
 
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.SetDenotator
contains, logicalEquals, subset, superset
 
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
getName, toString
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

SecondOrderVariable

public SecondOrderVariable()
Initialize a new second order variable. Its name consists of the letter 'V' and a number.


SecondOrderVariable

public SecondOrderVariable(String name)
Initialize a new second order variable with the given name.

Parameters:
name - The name of the variable.
Postcondition:
The name is set to the given name.
| new.getName() == name
Method Detail

forAll

public SecondOrderUniversalQuantification forAll(Formula form)
Returns the universal quantification of the given formula over this variable.

Parameters:
form - The formula to be quantified.
Precondition:
The given formula should be effective.
| form != null
Precondition:
This variable has to be free in the given formula.
| !form.containsVariable(this) || form.isFreeVariable(this);
Returns:
The universal quantification of the given formula over this variable.
| result.getBoundVariable() == this && | result.getArgument() == form

exists

public SecondOrderExistentialQuantification exists(Formula form)
Returns the existential quantification of the given formula over this variable.

Parameters:
form - The formula to be quantified.
Precondition:
The given formula should be effective.
| form != null
Precondition:
This variable has to be free in the given formula.
| !form.containsVariable(this) || form.isFreeVariable(this);
Returns:
The existential quantification of the given formula over this variable.
| result.getBoundVariable() == this && | result.getArgument() == form