

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object de.uni_tuebingen.sfb.lichtenstein.formulas.Variable de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderVariable
public final class FirstOrderVariable
A class representing first order variables in the monadic second order logic.
Field Summary 

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

name 
Method Summary  

Dominance 
dominates(FirstOrderVariable that)
Return the formula that says this variable dominates that variable. 
FirstOrderExistentialQuantification 
exists(Formula form)
Returns the existential quantification of the given formula over this variable. 
FirstOrderUniversalQuantification 
forAll(Formula form)
Returns the universal quantification of the given formula over this variable. 
static FirstOrderVariable 
getInstance(String name)
Factory method to get a variable. 
ImmediateDominance 
immediatelyDominates(FirstOrderVariable that)
Return the formula that says this variable immediately dominates that variable. 
Inclusion 
in(SetDenotator that)
Return the formula that says this variable is an element of that set. 
FirstOrderEquality 
logicalEquals(FirstOrderVariable that)
Return the formula that says this variable is equal to that variable. 
Precedence 
precedes(FirstOrderVariable that)
Return the formula that says this variable precedes that variable. 
ProperDominance 
properlyDominates(FirstOrderVariable that)
Return the formula that says this variable immediately dominates that variable. 
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 

public static FirstOrderVariable getInstance(String name)
name
 The name of the variable.public FirstOrderUniversalQuantification forAll(Formula form)
form
 The formula to be quantified.public FirstOrderExistentialQuantification exists(Formula form)
form
 The formula to be quantified.public FirstOrderEquality logicalEquals(FirstOrderVariable that)
that
 The other variable. That is a mnemonic for this.logicalEquals(that)
.public Inclusion in(SetDenotator that)
that
 The other variable. That is a mnemonic for this.in(that)
.public Dominance dominates(FirstOrderVariable that)
that
 The other variable. That is a mnemonic for this.dominates(that)
.public ImmediateDominance immediatelyDominates(FirstOrderVariable that)
that
 The other variable. That is a mnemonic for this.immediatelyDominates(that)
.public ProperDominance properlyDominates(FirstOrderVariable that)
that
 The other variable. That is a mnemonic for this.immediatelyDominates(that)
.public Precedence precedes(FirstOrderVariable that)
that
 The other variable. That is a mnemonic for this.precedes(that)
.


PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 