de.uni_tuebingen.sfb.lichtenstein.formulas
Class Implication

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.BinaryJunctor
              de.uni_tuebingen.sfb.lichtenstein.formulas.Implication

All Implemented Interfaces:

Formula, Visitable, Serializable

public final class Implication
extends BinaryJunctor

A class representing the implication of formulas.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

Implication(Formula antecedent, Formula consequent)
Initialize a new implication, given an antecedent and a consequent

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
Formula	getAntecedent() Return the antecedent of this implication.
Formula	getConsequent() Return the consequent of this implication.
Disjunction	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
String	getSymbol() Return the textual representation of this binary junctor.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.BinaryJunctor

computePredicates, computeVariables, containsVariable, equals, getFirstArgument, getNbSubformulas, getSecondArgument, getSubformulaAt, hashCode, isFree, toString

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula

getAllSubformulas

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl

and, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

Implication

public Implication(Formula antecedent,
                   Formula consequent)

Initialize a new implication, given an antecedent and a consequent

Parameters:

antecedent - The antecedent, i.e. the formula that implies.

consequent - The consequent, i.e. the implied formula.

Postconditions:

The antecedent is set to the given antecedent. | new.getAntecedent() == first

The consequent is set to the given consequent. | new.getConsequent() == second

Method Detail

getAntecedent

public Formula getAntecedent()

Return the antecedent of this implication.

Returns:

The antecedent is nothing but the first argument of this implication, viewed as a binary junctor. | result == getFirstArgument()

getConsequent

public Formula getConsequent()

Return the consequent of this implication.

Returns:

The consequent is nothing but the second argument of this implication, viewed as a binary junctor. | result == getFirstArgument()

getNormalForm

public Disjunction getNormalForm()

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

Returns:

The disjunction of the negation of the normal form of the antecedent and the normal form of the consequent. | result == getFirstArgument().getNormalForm().not().or(getSecondArgument().getNormalForm()) Note that this is similar to the disjunctive normal form, but not all the same!

getSymbol

public String getSymbol()

Return the textual representation of this binary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol LEFTWARD ARROW: → | result == "→"

accept

public void accept(FormulaVisitor visitor)
            throws VisitorException

Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.

Parameters:

visitor - The visitor that is to be accepted to do its work.

Throws:

VisitorException - [CAN] A visitor can throw an exception.