|
|||||||||
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.Formulas
public final class Formulas
A class containing convenience methods to create formulas.
Method Summary | |
---|---|
static Conjunction |
and(Formula... forms)
Return the conjunction of the given formula with that formula. |
static FirstOrderExistentialQuantification |
exists(FirstOrderVariable var,
Formula form)
Return the existential quantification of the given formula over the given first order variable. |
static SecondOrderExistentialQuantification |
exists(SecondOrderVariable var,
Formula form)
Return the existential quantification of the given formula over the given first order variable. |
static FirstOrderUniversalQuantification |
forAll(FirstOrderVariable var,
Formula form)
Return the universal quantification of the given formula over the given variable. |
static SecondOrderUniversalQuantification |
forAll(SecondOrderVariable var,
Formula form)
Return the universal quantification of the given formula over the given variable. |
static Equivalence |
iff(Formula first,
Formula second)
Return the equivalence of the given formula with that formula. |
static Implication |
implies(Formula first,
Formula second)
Return the implication of the first formula with the second formula. |
static Formula |
not(Formula form)
Return the negation of the given formula. |
static Disjunction |
or(Formula... forms)
Return the disjunction of the given formula with second formula. |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Method Detail |
---|
public static Formula not(Formula form)
form
- The formula to negate.| result.getArgument() == form
public static Conjunction and(Formula... forms)
forms
- The formulas to conjoin.| result.getFirstArgument() == first && |
result.getSecondArgument() == second
public static Disjunction or(Formula... forms)
forms
- The formulas to disjoin.| result.getFirstArgument() == first && |
result.getSecondArgument() == second
public static Implication implies(Formula first, Formula second)
first
- The antecedent.second
- The consequent.| result.getFirstArgument() == first && |
result.getSecondArgument() == second
public static Equivalence iff(Formula first, Formula second)
first
- The first formula.second
- The second formula.| result.getFirstArgument() == first && |
result.getSecondArgument() == second
public static FirstOrderUniversalQuantification forAll(FirstOrderVariable var, Formula form)
var
- The variable which is to be quantified.form
- The formula over which to quantify.| var != null &&
(!form.containsVariable(var)
|| form.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == form
public static SecondOrderUniversalQuantification forAll(SecondOrderVariable var, Formula form)
var
- The variable which is to be quantified.form
- The formula over which to quantify.| var != null &&
(!form.containsVariable(var)
|| form.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == form
public static FirstOrderExistentialQuantification exists(FirstOrderVariable var, Formula form)
var
- The variable which is to be quantified.form
- The formula over which to quantify.| var != null &&
(!form.containsVariable(var)
|| form.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == form
public static SecondOrderExistentialQuantification exists(SecondOrderVariable var, Formula form)
var
- The variable which is to be quantified.form
- The formula over which to quantify.| var != null &&
(!form.containsVariable(var)
|| form.isFreeVariable(var))
| result.getBoundVariable() == var && |
result.getArgument() == form
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |