|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
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
public class Negation
A class representing logical negation of a formula.
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 |
---|
containsVariable, equals, getArgument, getFirstIndexOf, getNbBoundVariables, getNbFreeVariables, getNbSubformulas, getNbVariables, getPredicates, getSubformulaAt, getVariableAt, hashCode, isFreeVariable, 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, getVariables, iff, implies, isClosed, or |
Methods inherited from class java.lang.Object |
---|
getClass, notify, notifyAll, wait, wait, wait |
Constructor Detail |
---|
public Negation(Formula negatedFormula)
negatedFormula
- The formula to be negated.| new.getNegatedFormula() == negatedFormula
Method Detail |
---|
public Formula not()
not
in interface Formula
not
in class FormulaImpl
public Formula getNegatedFormula()
| result == getArgument()
public Formula getNormalForm()
| result ==
getArgument().getNormalForm().not() TODO
public String getSymbol()
getSymbol
in class ComposedFormula
| result == "¬"
public void accept(FormulaVisitor visitor) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
accept
in interface Visitable
accept
in class FormulaImpl
visitor
- The visitor that is to be accepted to do its work.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |