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