|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface Formula
A class for specifying a formula in monadic second order logic.
formulas are immutable objects. TODO: extract more interfaces.
Method Summary | |
---|---|
Conjunction |
and(Formula that)
Return the conjunction of this formula with that formula. |
boolean |
containsVariable(Variable var)
Returns whether this formula contains the given variable. |
FirstOrderExistentialQuantification |
exists(FirstOrderVariable var)
Return the existential quantification of this formula over the given first order variable. |
SecondOrderExistentialQuantification |
exists(SecondOrderVariable var)
Return the existential quantification of this formula over the given first order variable. |
FirstOrderUniversalQuantification |
forAll(FirstOrderVariable var)
Return the universal quantification of this formula over the given variable. |
SecondOrderUniversalQuantification |
forAll(SecondOrderVariable var)
Return the universal quantification of this formula over the given variable. |
int |
getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs. |
Set<Variable> |
getFreeVariables()
Return the free variables in this formula. |
int |
getNbBoundVariables()
Returns the number of bound variables in this formula. |
int |
getNbFreeVariables()
Returns the number of free variables in this formula. |
int |
getNbVariables()
Returns the number of variables in this formula. |
Formula |
getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
Set<Predicate> |
getPredicates()
Return all predicates that occur in this formula. |
Variable |
getVariableAt(int index)
Get the indexth variable. |
Set<Variable> |
getVariables()
Return the variables in this formula. |
Equivalence |
iff(Formula that)
Return the equivalence of this formula with that formula. |
Implication |
implies(Formula that)
Return the implication of this formula with that formula. |
boolean |
isClosed()
Check whether this formula is closed. |
boolean |
isFreeVariable(Variable variable)
Check whether the given variable is free in this formula. |
Formula |
not()
Return the negation of this formula. |
Disjunction |
or(Formula that)
Return the disjunction of this formula with that formula. |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable |
---|
accept |
Method Detail |
---|
Formula not()
| result.getArgument() == this
Conjunction and(Formula that)
that
- The other formula. That is a mnemonic for this.and(that)
.| result.getFirstArgument() == this && |
result.getSecondArgument() == that
Disjunction or(Formula that)
that
- The other formula. That is a mnemonic for this.or(that)
.| result.getFirstArgument() == this && |
result.getSecondArgument() == that
Implication implies(Formula that)
that
- The other formula. That is a mnemonic for this.implies(that)
.| result.getFirstArgument() == this && |
result.getSecondArgument() == that
Equivalence iff(Formula that)
that
- The other formula. That is a mnemonic for this.iff(that)
.| result.getFirstArgument() == this && |
result.getSecondArgument() == that
FirstOrderUniversalQuantification forAll(FirstOrderVariable var)
var
- The variable which is to be quantified.| var != null &&
(!this.containsVariable(var)
|| this.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == this
SecondOrderUniversalQuantification forAll(SecondOrderVariable var)
var
- The variable which is to be quantified.| var != null &&
(!this.containsVariable(var)
|| this.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == this
FirstOrderExistentialQuantification exists(FirstOrderVariable var)
var
- The variable which is to be quantified.| var != null &&
(!this.containsVariable(var)
|| this.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == this
SecondOrderExistentialQuantification exists(SecondOrderVariable var)
var
- The variable which is to be quantified.| var != null &&
(!this.containsVariable(var)
|| this.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == this
int getNbFreeVariables()
| result == card(var : isFreeVariable(var) &&
containsVariable(var))
Set<Variable> getVariables()
LinkedHashSet
Set<Variable> getFreeVariables()
int getNbBoundVariables()
| result == card(var : ! isFreeVariable(var) &&
containsVariable(var))
int getNbVariables()
int getFirstIndexOf(Variable var)
var
- The variable of which the index is wanted.| containsVariable(var)
|
getVariableAt(result).equals(index)
Variable getVariableAt(int index) throws IndexOutOfBoundsException
index
- The index of the wanted variable
| index <
0
|| index >= getNbVariables()
boolean containsVariable(Variable var)
var
- The variable to check.
boolean isFreeVariable(Variable variable)
variable
- The variable to check.
Set<Predicate> getPredicates()
Formula getNormalForm()
This is a notion of normal form mainly useful for my program. BAD!
TODO: standardize this.
| for form in getAllSubformulas() | form in AtomicFormula || |
form in Disjunction
|| | form in Conjunction || | form in Negation || | form in ExistentialQuantification
boolean isClosed()
| result == getNbFreeVariables() == 0
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |