de.uni_tuebingen.sfb.lichtenstein.formulas
Class Formulas

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.Formulas

public final class Formulas
extends Object

A class containing convenience methods to create formulas.

Author:
Hendrik Maryns

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

not

public static Formula not(Formula form)
Return the negation of the given formula.

Parameters:
form - The formula to negate.
Returns:
The negation of the given formula.
| result.getArgument() == form

and

public static Conjunction and(Formula... forms)
Return the conjunction of the given formula with that formula.

Parameters:
forms - The formulas to conjoin.
Returns:
The conjunction of the given formulas.
| result.getFirstArgument() == first && | result.getSecondArgument() == second

or

public static Disjunction or(Formula... forms)
Return the disjunction of the given formula with second formula.

Parameters:
forms - The formulas to disjoin.
Returns:
The disjunction of the given formulas.
| result.getFirstArgument() == first && | result.getSecondArgument() == second

implies

public static Implication implies(Formula first,
                                  Formula second)
Return the implication of the first formula with the second formula.

Parameters:
first - The antecedent.
second - The consequent.
Returns:
The implication of the second formula by the first formula.
| result.getFirstArgument() == first && | result.getSecondArgument() == second

iff

public static Equivalence iff(Formula first,
                              Formula second)
Return the equivalence of the given formula with that formula.

Parameters:
first - The first formula.
second - The second formula.
Returns:
The equivalence of the given formulas.
| result.getFirstArgument() == first && | result.getSecondArgument() == second

forAll

public static FirstOrderUniversalQuantification forAll(FirstOrderVariable var,
                                                       Formula form)
Return the universal quantification of the given formula over the given variable.

Parameters:
var - The variable which is to be quantified.
form - The formula over which to quantify.
Precondition:
The given variable must be effective and the variable must not be bound in the given formula.
| var != null && (!form.containsVariable(var) || form.isFreeVariable(var))
Returns:
The universal quantification over the given variable.
| result.getBoundVariable() == var && | result.getArgument() == form

forAll

public static SecondOrderUniversalQuantification forAll(SecondOrderVariable var,
                                                        Formula form)
Return the universal quantification of the given formula over the given variable.

Parameters:
var - The variable which is to be quantified.
form - The formula over which to quantify.
Precondition:
The given variable must be effective and the variable must not be bound in the given formula.
| var != null && (!form.containsVariable(var) || form.isFreeVariable(var))
Returns:
The universal quantification over the given variable.
| result.getBoundVariable() == var && | result.getArgument() == form

exists

public static FirstOrderExistentialQuantification exists(FirstOrderVariable var,
                                                         Formula form)
Return the existential quantification of the given formula over the given first order variable.

Parameters:
var - The variable which is to be quantified.
form - The formula over which to quantify.
Precondition:
The given variable must be effective and the variable must not be bound in the given formula.
| var != null && (!form.containsVariable(var) || form.isFreeVariable(var))
Returns:
The existential quantification over the given variable.
| result.getBoundVariable() == var && | result.getArgument() == form

exists

public static SecondOrderExistentialQuantification exists(SecondOrderVariable var,
                                                          Formula form)
Return the existential quantification of the given formula over the given first order variable.

Parameters:
var - The variable which is to be quantified.
form - The formula over which to quantify.
Precondition:
The given variable must be effective and the variable must not be bound in the given formula.
| var != null && (!form.containsVariable(var) || form.isFreeVariable(var))
Returns:
The existential quantification over the given variable.
| result.getBoundVariable() == var && | result.getArgument() == form