Class 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.
Matthias Thimm
  • Constructor Details

    • Necessity

      public Necessity(RelationalFormula formula)
      Creates a new necessity formula with the given inner formula
      formula - a formula, either a modal formula or a first-order formula.
  • Method Details

    • substitute

      public FolFormula substitute(Term<?> v, Term<?> t) throws 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 interface ComplexLogicalFormula
      Specified by:
      substitute in class FolFormula
      v - the term to be substituted.
      t - the term to substitute.
      a formula where every occurrence of "v" is replaced by "t".
      IllegalArgumentException - if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
    • toString

      public String toString()
      Specified by:
      toString in class RelationalFormula
    • clone

      public FolFormula clone()
      Description copied from interface: SimpleLogicalFormula
      Creates a deep copy of this formula
      Specified by:
      clone in interface ComplexLogicalFormula
      Specified by:
      clone in interface SimpleLogicalFormula
      Specified by:
      clone in class FolFormula
      the cloned formula
    • toNnf

      public FolFormula toNnf()
      Description copied from class: FolFormula
      Makes the negation normal form of this formula.
      Specified by:
      toNnf in class FolFormula
      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 class FolFormula
      "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 class FolFormula
      the collapsed formula.