de.uni_tuebingen.sfb.lichtenstein.formulas
Interface Formula

All Superinterfaces:

Serializable, Visitable

All Known Subinterfaces:

Quantification

All Known Implementing Classes:

AtomicFormula, BinaryJunctor, ComposedFormula, Conjunction, Disjunction, Dominance, Equivalence, FirstOrderEquality, FirstOrderExistentialQuantification, FirstOrderQuantor, FirstOrderUniversalQuantification, FormulaImpl, ImmediateDominance, Implication, Inclusion, NaryJunctor, Negation, Precedence, ProperDominance, SecondOrderEquality, SecondOrderExistentialQuantification, SecondOrderQuantor, SecondOrderUniversalQuantification, Subset, UnaryJunctor

public interface Formula
extends Visitable, Serializable

A class for specifying a formula in monadic second order logic.

formulas are immutable objects. TODO: extract more interfaces.

Author:

Hendrik Maryns

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

not

Formula not()

Return the negation of this formula.

Returns:

The negation of this formula.

| result.getArgument() == this

and

Conjunction and(Formula that)

Return the conjunction of this formula with that formula.

Parameters:

that - The other formula. That is a mnemonic for this.and(that).

Returns:

The conjunction of this formula and that formula.

| result.getFirstArgument() == this && |
         result.getSecondArgument() == that

or

Disjunction or(Formula that)

Return the disjunction of this formula with that formula.

Parameters:

that - The other formula. That is a mnemonic for this.or(that).

Returns:

The disjunction of this formula and that formula.

| result.getFirstArgument() == this && |
         result.getSecondArgument() == that

implies

Implication implies(Formula that)

Return the implication of this formula with that formula.

Parameters:

that - The other formula. That is a mnemonic for this.implies(that).

Returns:

The implication of that formula by this formula.

| result.getFirstArgument() == this && |
         result.getSecondArgument() == that

iff

Equivalence iff(Formula that)

Return the equivalence of this formula with that formula.

Parameters:

that - The other formula. That is a mnemonic for this.iff(that).

Returns:

The equivalence of this formula and that formula.

| result.getFirstArgument() == this && |
         result.getSecondArgument() == that

forAll

FirstOrderUniversalQuantification forAll(FirstOrderVariable var)

Return the universal quantification of this formula over the given variable.

Parameters:

var - The variable which is to be quantified.

Precondition:

The given variable must be effective and the variable must not be bound in this formula.

| var != null &&
      (!this.containsVariable(var)
|| this.isFreeVariable(var))

Returns:

The universal quantification over the given variable.

| result.getBoundVariable() == var && |
         result.getArgument() == this

forAll

SecondOrderUniversalQuantification forAll(SecondOrderVariable var)

Return the universal quantification of this formula over the given variable.

Parameters:

var - The variable which is to be quantified.

Precondition:

The given variable must be effective and the variable must not be bound in this formula.

| var != null &&
      (!this.containsVariable(var)
|| this.isFreeVariable(var))

Returns:

The universal quantification over the given variable.

| result.getBoundVariable() == var && |
         result.getArgument() == this

exists

FirstOrderExistentialQuantification exists(FirstOrderVariable var)

Return the existential quantification of this formula over the given first order variable.

Parameters:

var - The variable which is to be quantified.

Precondition:

The given variable must be effective and the variable must not be bound in this formula.

| var != null &&
      (!this.containsVariable(var)
|| this.isFreeVariable(var))

Returns:

The existential quantification over the given variable.

| result.getBoundVariable() == var && |
         result.getArgument() == this

exists

SecondOrderExistentialQuantification exists(SecondOrderVariable var)

Return the existential quantification of this formula over the given first order variable.

Parameters:

var - The variable which is to be quantified.

Precondition:

The given variable must be effective and the variable must not be bound in this formula.

| var != null &&
      (!this.containsVariable(var)
|| this.isFreeVariable(var))

Returns:

The existential quantification over the given variable.

| result.getBoundVariable() == var && |
         result.getArgument() == this

getNbFreeVariables

int getNbFreeVariables()

Returns the number of free variables in this formula.

Returns:

The number of variables in this formula which are free.

| result == card(var : isFreeVariable(var) &&
         containsVariable(var))

getVariables

Set<Variable> getVariables()

Return the variables in this formula. They are guaranteed to be returned by the iterator in the same order as they appear in the formula.

See Also:

LinkedHashSet

Returns:

A set with the variables in the order of occurrence in the formula.

getFreeVariables

Set<Variable> getFreeVariables()

Return the free variables in this formula.

Returns:

The free variables.

getNbBoundVariables

int getNbBoundVariables()

Returns the number of bound variables in this formula.

Returns:

The number of variables in this formula which are bound.

| result == card(var : ! isFreeVariable(var) &&
         containsVariable(var))

getNbVariables

int getNbVariables()

Returns the number of variables in this formula.

Returns:

The number of variables.

getFirstIndexOf

int getFirstIndexOf(Variable var)

Get the first index at which the given variable occurs.

Parameters:

var - The variable of which the index is wanted.

Precondition:

This formula must contain the variable.

| containsVariable(var)

Returns:

The variable at the resulting index is the same as the given variable.

|
         getVariableAt(result).equals(index)

getVariableAt

Variable getVariableAt(int index)
                       throws IndexOutOfBoundsException

Get the indexth variable.

Parameters:

index - The index of the wanted variable

Returns:

The variable at the given index.

Throws:

IndexOutOfBoundsException

The index is bigger than or equal to the number of variables in this formula, or less than zero

| index <
         0
|| index >= getNbVariables()

containsVariable

boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

Returns:

Whether the given variable occurs in the formula.

isFreeVariable

boolean isFreeVariable(Variable variable)

Check whether the given variable is free in this formula.

Parameters:

variable - The variable to check.

Returns:

True if the variable occurs in the formula and is not bound by an existential or universal quantifier.

getPredicates

Set<Predicate> getPredicates()

Return all predicates that occur in this formula. TODO

Returns:

The predicates that occur in the formula.

getNormalForm

Formula getNormalForm()

Get a normal form with only conjunction, disjunction, negation and existential quantification.

This is a notion of normal form mainly useful for my program. BAD!

TODO: standardize this.

Returns:

A formula only containing or, not and exists.

| for form in getAllSubformulas() | form in AtomicFormula || |
         form in Disjunction
|| | form in Conjunction || | form in Negation || | form in ExistentialQuantification

isClosed

boolean isClosed()

Check whether this formula is closed.

Returns:

A formula is closed if it has no free variables.

| result == getNbFreeVariables() == 0