de.uni_tuebingen.sfb.lichtenstein.formulas
Class Negation

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.UnaryJunctor
              de.uni_tuebingen.sfb.lichtenstein.formulas.Negation

All Implemented Interfaces:

Formula, Visitable, Serializable

public final class Negation
extends UnaryJunctor

A class representing logical negation of a formula.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

Negation(Formula negatedFormula)
Initialize a new negation, given the formula to be negated.

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
Formula	getNegatedFormula() Returns the negated formula.
Formula	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
String	getSymbol() Return the textual representation of this unary junctor.
Formula	not() The negation of a negation is the formula itself.

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

computePredicates, computeVariables, containsVariable, equals, getArgument, getNbSubformulas, 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, or

Methods inherited from class java.lang.Object

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

Constructor Detail

Negation

public Negation(Formula negatedFormula)

Initialize a new negation, given the formula to be negated.

Parameters:

negatedFormula - The formula to be negated.

Postcondition:

The negated formula is set to the given formula. | new.getNegatedFormula() == negatedFormula

Method Detail

not

public Formula not()

The negation of a negation is the formula itself.

Specified by:

not in interface Formula

Overrides:

not in class FormulaImpl

Returns:

The argument formula.

getNegatedFormula

public Formula getNegatedFormula()

Returns the negated formula.

Returns:

The negated formula is the argument of the negation. | result == getArgument()

getNormalForm

public Formula getNormalForm()

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

Returns:

The negation of the normal form of the argument or an equivalent logical formula. | result == getArgument().getNormalForm().not() TODO

getSymbol

public String getSymbol()

Return the textual representation of this unary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol NOT SIGN: ¬. | 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.