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, ImmediatePrecedence, 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.
Set<Variable>	getFreeVariables() Return the free 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.
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	isFree(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

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:

The set of variables in the order of occurrence in the formula.

getFreeVariables

Set<Variable> getFreeVariables()

Return the free variables in this formula.

See Also:

LinkedHashSet

Returns:

The set of free variables in the order of occurrence in the formula.

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.

isFree

boolean isFree(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