de.uni_tuebingen.sfb.lichtenstein.formulas
Class SecondOrderVariable

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
      de.uni_tuebingen.sfb.lichtenstein.formulas.SetDenotator
          de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderVariable

All Implemented Interfaces:

Serializable

public final class SecondOrderVariable
extends SetDenotator

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

Author:

Hendrik Maryns

See Also:

Serialized Form

Field Summary

Fields inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable

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.
static SecondOrderVariable	getInstance(String name) Factory method to get a 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

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

getInstance

public static SecondOrderVariable getInstance(String name)

Factory method to get a variable. If a variable with the given name already exists, it is returned.

Parameters:

name - The name of the variable.

Returns:

The unique variable with the given name. If the name is not effective, a variable with a random name is returned. | if ( name != null ) | then result.getName() == name

forAll

public SecondOrderUniversalQuantification forAll(Formula form)

Returns the universal quantification of the given formula over this variable.

Parameters:

form - The formula to be quantified.

Preconditions:

The given formula should be effective. | form != null

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.

Preconditions:

The given formula should be effective. | form != null

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