|
|||||||||
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 class FirstOrderVariable
A class representing first order variables in the monadic second order logic.
Constructor Summary | |
---|---|
FirstOrderVariable()
Initialize a new first order variable. |
|
FirstOrderVariable(String name)
Initialize a first order variable with the given 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. |
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 |
---|
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Constructor Detail |
---|
public FirstOrderVariable()
public FirstOrderVariable(String name)
name
- The name of the variable.| new.getName() == name
Method Detail |
---|
public FirstOrderUniversalQuantification forAll(Formula form)
form
- The formula to be quantified.| form != null
| !form.containsVariable(this) ||
form.isFreeVariable(this);
| result.getBoundVariable() == this && |
result.getArgument() == form
public FirstOrderExistentialQuantification exists(Formula form)
form
- The formula to be quantified.| form != null
| !form.containsVariable(this) ||
form.isFreeVariable(this);
| result.getBoundVariable() ==
this &&
| result.getArgument() == form
public FirstOrderEquality logicalEquals(FirstOrderVariable that)
that
- The other variable. That is a mnemonic for this.logicalEquals(that)
.| result.getFirstVariable() == this && |
result.getSecondVariable() == that
public Inclusion in(SetDenotator that)
that
- The other variable. That is a mnemonic for this.in(that)
.| result.getIncludedVariable() ==
this &&
| result.getContainingVariable() == that
public Dominance dominates(FirstOrderVariable that)
that
- The other variable. That is a mnemonic for this.dominates(that)
.| result.getDominatingVariable() ==
this &&
| result.getDominatedVariable() == that
public ImmediateDominance immediatelyDominates(FirstOrderVariable that)
that
- The other variable. That is a mnemonic for this.immediatelyDominates(that)
.|
result.getDominatingVariable() == this &&
| result.getDominatedVariable() == that
public ProperDominance properlyDominates(FirstOrderVariable that)
that
- The other variable. That is a mnemonic for this.immediatelyDominates(that)
.|
result.getDominatingVariable() == this &&
| result.getDominatedVariable() == that
public Precedence precedes(FirstOrderVariable that)
that
- The other variable. That is a mnemonic for this.precedes(that)
.| result.getPrecedingVariable() == this && |
result.getPrecededVariable() == that
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |