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 |
---|---|
RelationalFormula |
clone()
Creates a deep copy of this formula
|
RelationalFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
java.lang.String |
toString() |
combineWithAnd, combineWithOr, complement, containsQuantifier, equals, getAtoms, getFormula, getFunctors, getPredicates, getQuantifierVariables, getSignature, getTerms, getTerms, getUnboundVariables, getUniformProbability, hashCode, isClosed, isClosed, isLiteral, isWellBound, isWellBound
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 RelationalFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class ModalFormula
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 RelationalFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class RelationalFormula