public final class FormulaProposition extends Formula
Modifier and Type | Method and Description |
---|---|
Formula |
applyIntuitionisticPartialSubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution as
intuitionistic partial substitution.
|
Formula |
applySubstitution(PropositionalSubstitution subst)
Returns the formula obtained by applying the specified substitution on
propositional formulas.
|
Formula |
applySubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution.
|
Formula |
calculateBooleanSimplification()
Returns the formula obtained by applying boolean simplifications on this
formula.
|
boolean |
containsFalse()
Returns
true iff this formula contains the propositional
constant FALSE as subformula. |
boolean |
containsProposition(FormulaProposition proposition)
Returns
true iff this formula contains the specified
propositional formula as subformula. |
boolean |
containsTrue()
Returns
true iff this formula contains the propositional
constant TRUE as subfromula. |
boolean |
equals(java.lang.Object other) |
java.lang.String |
format()
Returns the string representation of the formula
|
FormulaFactory |
getFactory()
Returns the factory used to build this formula.
|
FormulaType |
getFormulaType()
Returns the formula type of this formula.
|
java.lang.String |
getName() |
int |
hashCode() |
Formula[] |
immediateSubformulas()
The subformulas of this formula.
|
boolean |
isAtomic()
Returns
true iff this formula is atomic. |
boolean |
isCompound()
Returns
true iff this formula is compound. |
boolean |
isFalse()
Returns
true iff this propositional formula represents FALSE. |
boolean |
isIntuitionisticLocalFormula()
TODO: doc Returns
true iff this is a local formula. |
boolean |
isTrue()
Returns
true iff this propositional formula represents TRUE. |
PropositionalConnective |
mainConnective()
The main logical operator of this formula.
|
java.lang.String |
shortName()
Returns the short name of the formula.
|
java.lang.String |
toString() |
public FormulaFactory getFactory()
Formula
getFactory
in class Formula
public java.lang.String getName()
public java.lang.String shortName()
_AbstractFormula
public Formula calculateBooleanSimplification()
Formula
calculateBooleanSimplification
in class Formula
public Formula applySubstitution(PropositionalSubstitution subst)
Formula
applySubstitution
in class Formula
subst
- the substitution to apply.public Formula applySubstitution(Substitution subst)
Formula
applySubstitution
in class Formula
subst
- the substitution to apply.public Formula applyIntuitionisticPartialSubstitution(Substitution subst)
Formula
applyIntuitionisticPartialSubstitution
in class Formula
subst
- the substitution to apply.public boolean isAtomic()
_PropositionalFormula
true
iff this formula is atomic.true
iff this formula is atomic.public boolean isCompound()
_PropositionalFormula
true
iff this formula is compound.true
iff this formula is compound.public PropositionalConnective mainConnective()
_PropositionalFormula
public Formula[] immediateSubformulas()
Formula
immediateSubformulas
in interface _PropositionalFormula
immediateSubformulas
in class Formula
public java.lang.String format()
_AbstractFormula
public java.lang.String toString()
toString
in class java.lang.Object
public boolean containsProposition(FormulaProposition proposition)
Formula
true
iff this formula contains the specified
propositional formula as subformula.proposition
- the propositional formula.true
iff this formula contains the specified
proposition.public boolean containsTrue()
Formula
true
iff this formula contains the propositional
constant TRUE as subfromula.containsTrue
in class Formula
true
iff this formula contains the propositional
constant TRUE.public boolean containsFalse()
Formula
true
iff this formula contains the propositional
constant FALSE as subformula.containsFalse
in class Formula
true
iff this formula contains the propositional
constant FALSE.public boolean isFalse()
true
iff this propositional formula represents FALSE.public boolean isTrue()
true
iff this propositional formula represents TRUE.public boolean isIntuitionisticLocalFormula()
Formula
true
iff this is a local formula.isIntuitionisticLocalFormula
in class Formula
true
iff this is a local formula.public FormulaType getFormulaType()
Formula
getFormulaType
in class Formula