public abstract class Formula extends java.lang.Object implements _PropositionalFormula
Modifier and Type | Method and Description |
---|---|
abstract Formula |
applyIntuitionisticPartialSubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution as
intuitionistic partial substitution.
|
abstract Formula |
applySubstitution(PropositionalSubstitution subst)
Returns the formula obtained by applying the specified substitution on
propositional formulas.
|
abstract Formula |
applySubstitution(Substitution subst)
Returns the formula obtained by applying the specified substitution.
|
abstract Formula |
calculateBooleanSimplification()
Returns the formula obtained by applying boolean simplifications on this
formula.
|
abstract boolean |
containsFalse()
Returns
true iff this formula contains the propositional
constant FALSE as subformula. |
abstract boolean |
containsTrue()
Returns
true iff this formula contains the propositional
constant TRUE as subfromula. |
boolean |
equals(java.lang.Object obj) |
abstract FormulaFactory |
getFactory()
Returns the factory used to build this formula.
|
abstract FormulaType |
getFormulaType()
Returns the formula type of this formula.
|
int |
getIndex()
Returns the index for this formula.
|
int |
hashCode() |
abstract Formula[] |
immediateSubformulas()
The subformulas of this formula.
|
abstract boolean |
isFalse()
Returns
true iff this formula is the propositional constant
FALSE. |
abstract boolean |
isIntuitionisticLocalFormula()
TODO: doc Returns
true iff this is a local formula. |
abstract boolean |
isTrue()
Returns
true iff this is the propositional constant TRUE. |
int |
size()
Returns the size of this formula.
|
getClass, notify, notifyAll, toString, wait, wait, wait
isAtomic, isCompound, mainConnective
format, shortName
public int getIndex()
public abstract Formula[] immediateSubformulas()
immediateSubformulas
in interface _PropositionalFormula
public abstract Formula calculateBooleanSimplification()
public abstract Formula applySubstitution(PropositionalSubstitution subst)
subst
- the substitution to apply.public abstract Formula applySubstitution(Substitution subst)
subst
- the substitution to apply.public abstract Formula applyIntuitionisticPartialSubstitution(Substitution subst)
subst
- the substitution to apply.public abstract boolean containsTrue()
true
iff this formula contains the propositional
constant TRUE as subfromula.true
iff this formula contains the propositional
constant TRUE.public abstract boolean containsFalse()
true
iff this formula contains the propositional
constant FALSE as subformula.true
iff this formula contains the propositional
constant FALSE.public abstract boolean isFalse()
true
iff this formula is the propositional constant
FALSE.true
iff this formula is the propositional constant
FALSE.public abstract boolean isTrue()
true
iff this is the propositional constant TRUE.true
iff this is the propositional constant TRUE.public abstract boolean isIntuitionisticLocalFormula()
true
iff this is a local formula.true
iff this is a local formula.public abstract FormulaFactory getFactory()
public abstract FormulaType getFormulaType()
public int size()
public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object