de.uni_tuebingen.sfb.lichtenstein.formulas
Class Formulas

java.lang.Object
  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