Package net.sf.tweety.logics.ml.syntax
Class Necessity
- java.lang.Object
-
- net.sf.tweety.logics.commons.syntax.RelationalFormula
-
- net.sf.tweety.logics.fol.syntax.FolFormula
-
- net.sf.tweety.logics.ml.syntax.MlFormula
-
- net.sf.tweety.logics.ml.syntax.Necessity
-
- All Implemented Interfaces:
Formula
,ClassicalFormula
,ComplexLogicalFormula
,Conjunctable
,Disjunctable
,Invertable
,LogicStructure
,ProbabilityAware
,QuantifiedFormula
,SimpleLogicalFormula
public class Necessity extends MlFormula
This class models the necessity modality.- Author:
- Matthias Thimm
-
-
Constructor Summary
Constructors Constructor Description Necessity(RelationalFormula formula)
Creates a new necessity formula with the given inner formula
-
Method Summary
Modifier and Type Method Description FolFormula
clone()
Creates a deep copy of this formulaRelationalFormula
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()
-
Methods inherited from class net.sf.tweety.logics.ml.syntax.MlFormula
combineWithAnd, combineWithOr, complement, containsModalityOperator, containsQuantifier, equals, getAtoms, getFormula, getFunctors, getPredicates, getQuantifierVariables, getSignature, getTerms, getTerms, getUnboundVariables, getUniformProbability, hashCode, isClosed, isClosed, isLiteral, isWellBound, isWellBound
-
Methods inherited from class net.sf.tweety.logics.fol.syntax.FolFormula
toDnf
-
Methods inherited from class net.sf.tweety.logics.commons.syntax.RelationalFormula
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute
-
-
-
-
Constructor Detail
-
Necessity
public Necessity(RelationalFormula formula)
Creates a new necessity formula with the given inner formula- Parameters:
formula
- a formula, either a modal formula or a first-order formula.
-
-
Method Detail
-
substitute
public FolFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
Description copied from class:RelationalFormula
Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.- Specified by:
substitute
in interfaceComplexLogicalFormula
- Specified by:
substitute
in classFolFormula
- Parameters:
v
- the term to be substituted.t
- the term to substitute.- Returns:
- a formula where every occurrence of "v" is replaced by "t".
- Throws:
java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
-
toString
public java.lang.String toString()
- Specified by:
toString
in classRelationalFormula
-
clone
public FolFormula clone()
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceComplexLogicalFormula
- Specified by:
clone
in interfaceSimpleLogicalFormula
- Specified by:
clone
in classFolFormula
- Returns:
- the cloned formula
-
toNnf
public FolFormula toNnf()
Description copied from class:FolFormula
Makes the negation normal form of this formula.- Specified by:
toNnf
in classFolFormula
- Returns:
- the NNF of this formula
-
isDnf
public boolean isDnf()
Description copied from class:FolFormula
Checks whether this formula is in disjunctive normal form.- Specified by:
isDnf
in classFolFormula
- Returns:
- "true" iff this formula is in disjunctive normal form.
-
collapseAssociativeFormulas
public RelationalFormula collapseAssociativeFormulas()
Description copied from class:FolFormula
This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.- Specified by:
collapseAssociativeFormulas
in classFolFormula
- Returns:
- the collapsed formula.
-
-