Package org.tweetyproject.logics.fol.syntax

Class FolFormula

java.lang.Object
org.tweetyproject.logics.commons.syntax.RelationalFormula
org.tweetyproject.logics.fol.syntax.FolFormula
All Implemented Interfaces:
Formula, ClassicalFormula, ComplexLogicalFormula, Conjunctable, Disjunctable, Invertable, LogicStructure, ProbabilityAware, QuantifiedFormula, SimpleLogicalFormula
Direct Known Subclasses:
AssociativeFolFormula, Equivalence, ExistsQuantifiedFormula, FolAtom, ForallQuantifiedFormula, Implication, MlFormula, Negation, NLPNot, SpecialFormula
public abstract class FolFormula extends RelationalFormula
The common abstract class for formulas of first-order logic. NOTE: "RelationalFormula" and "FolFormula" differ in their meaning as follows:
  • A relational formula is any formula over a first-order signature, i.e. even a conditional
  • A first-order formula is the actual first-order formula in the classical sense.
Author:
Matthias Thimm, Tim Janus

  • Constructor Details

    • FolFormula

      public FolFormula()

  • Method Details

    • combineWithAnd

      public Conjunction combineWithAnd(Conjunctable f)
      Description copied from interface: Conjunctable
      Returns a conjunction of this and the given formula.
      Specified by:
      combineWithAnd in interface Conjunctable
      Specified by:
      combineWithAnd in class RelationalFormula
      Parameters:
      f - a formula to be combined with AND and this.
      Returns:
      a conjunction of this and the given formula.

    • combineWithOr

      public Disjunction combineWithOr(Disjunctable f)
      Specified by:
      combineWithOr in interface Disjunctable
      Specified by:
      combineWithOr in class RelationalFormula
      Parameters:
      f - a formula to be combined with OR and this.
      Returns:
      a disjunction of this and the given formula.

    • complement

      public RelationalFormula complement()
      Specified by:
      complement in interface Invertable
      Specified by:
      complement in class RelationalFormula
      Returns:
      the complement of this formula.

    • getQuantifierVariables

      public Set<Variable> getQuantifierVariables()
      Returns:
      a set containing all quantified variables

    • toDnf

      public FolFormula toDnf()
      Makes a disjunctive normal form of this formula.
      Returns:
      the DNF of this formula

    • toNnf

      public abstract FolFormula toNnf()
      Makes the negation normal form of this formula.
      Returns:
      the NNF of this formula

    • collapseAssociativeFormulas

      public abstract RelationalFormula collapseAssociativeFormulas()
      This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.
      Returns:
      the collapsed formula.

    • getUniformProbability

      public Probability getUniformProbability()
      Specified by:
      getUniformProbability in interface ProbabilityAware
      Specified by:
      getUniformProbability in class RelationalFormula
      Returns:
      this formula's probability in the uniform distribution.

    • isDnf

      public abstract boolean isDnf()
      Checks whether this formula is in disjunctive normal form.
      Returns:
      "true" iff this formula is in disjunctive normal form.

    • substitute

      public abstract 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 RelationalFormula
      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:
      IllegalArgumentException - if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).

    • clone

      public abstract 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 RelationalFormula
      Returns:
      the cloned formula

    • getSignature

      public FolSignature getSignature()
      Description copied from interface: Formula
      Returns the signature of the language of this formula.
      Returns:
      the signature of the language of this formula.