public class Necessity extends ModalFormula
Constructor and Description |
---|
Necessity(RelationalFormula formula)
Creates a new necessity formula with the
given inner formula
|
Modifier and Type | Method and Description |
---|---|
FolFormula |
clone()
Creates a deep copy of this formula
|
RelationalFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
boolean |
isDnf()
Checks whether this formula is in disjunctive normal form.
|
FolFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
FolFormula |
toNnf()
Makes the negation normal form of this formula.
|
java.lang.String |
toString() |
combineWithAnd, combineWithOr, complement, containsModalityOperator, containsQuantifier, equals, getAtoms, getFormula, getFunctors, getPredicates, getQuantifierVariables, getSignature, getTerms, getTerms, getUnboundVariables, getUniformProbability, hashCode, isClosed, isClosed, isLiteral, isWellBound, isWellBound
toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute
public Necessity(RelationalFormula formula)
formula
- a formula, either a modal formula or a first-order formula.public FolFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class FolFormula
v
- the term to be substituted.t
- the term to substitute.java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts
(NOTE: this exception is only thrown when "v" actually appears in this
formula).public java.lang.String toString()
toString
in class RelationalFormula
public FolFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class FolFormula
public FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public RelationalFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
public boolean isDnf()
FolFormula
isDnf
in class FolFormula