Class RelationalFormula

java.lang.Object
org.tweetyproject.logics.commons.syntax.RelationalFormula
All Implemented Interfaces:
Formula, ClassicalFormula, ComplexLogicalFormula, Conjunctable, Disjunctable, Invertable, LogicStructure, ProbabilityAware, QuantifiedFormula, SimpleLogicalFormula
Direct Known Subclasses:
DefaultRule, DelpRule, FolFormula, MlnFormula, RelationalConditional
public abstract class RelationalFormula extends Object implements ClassicalFormula, QuantifiedFormula
This is the abstract base class for relational formulas, i.e. formulas that are build on first-order signatures. 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, Anna Gessler

  • Constructor Details

    • RelationalFormula

      public RelationalFormula()

  • Method Details

    • getFormula

      public RelationalFormula getFormula()
      Specified by:
      getFormula in interface QuantifiedFormula
      Returns:
      the relational formula

    • getAtoms

      public abstract Set<? extends Atom> getAtoms()
      Description copied from interface: SimpleLogicalFormula
      Processes the set of all atoms which appear in this formula
      Specified by:
      getAtoms in interface SimpleLogicalFormula
      Returns:
      all atoms that appear in this formula.

    • getFunctors

      public abstract Set<Functor> getFunctors()
      Returns:
      all functors that appear in this formula.

    • getPredicateCls

      public Class<? extends Predicate> getPredicateCls()
      Specified by:
      getPredicateCls in interface SimpleLogicalFormula
      Returns:
      The class description of the predicate used by this formula.

    • substitute

      public abstract RelationalFormula substitute(Term<?> v, Term<?> t) throws IllegalArgumentException
      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
      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).

    • substitute

      public RelationalFormula substitute(Map<? extends Term<?>,? extends Term<?>> map) throws IllegalArgumentException
      Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
      NOTE: variables bound to quantifiers are not substituted in their inner formulas even if they appear in the map.
      Specified by:
      substitute in interface ComplexLogicalFormula
      Parameters:
      map - a mapping defining which terms to be substituted.
      Returns:
      a formula where every term in map.keyset() has been replaced by map.get(v).
      Throws:
      IllegalArgumentException - if any term and its mapping are of different sorts (NOTE: this exception is only thrown when the variable actually appears in this formula).

    • exchange

      public RelationalFormula exchange(Term<?> v, Term<?> t) throws IllegalArgumentException
      Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually 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:
      exchange in interface ComplexLogicalFormula
      Parameters:
      v - a term.
      t - a term.
      Returns:
      a new relational formula with both "v" and "t" exchanged.
      Throws:
      IllegalArgumentException - if "v" and "t" are of different sorts

    • allSubstitutions

      public Set<Map<Variable,Term<?>>> allSubstitutions(Collection<? extends Term<?>> terms) throws IllegalArgumentException
      Computes all possible substitutions, i.e. maps from variables to terms, of unbound variables of this formula to terms in "terms".
      Parameters:
      terms - a set of terms.
      Returns:
      a set of maps from variables to terms.
      Throws:
      IllegalArgumentException - if there is an unbound variable in this formula for which there is no term in "terms" with the same sort.

    • allGroundInstances

      public Set<RelationalFormula> allGroundInstances(Set<Constant> constants) throws IllegalArgumentException
      Computes all ground instances of this relational formula wrt. the given set of constants, i.e. every formula where each occurrence of some unbound variable is replaced by some constant.
      Parameters:
      constants - a set of constants
      Returns:
      a set of ground instances of this formula
      Throws:
      IllegalArgumentException - if there is an unbound variable in this formula for which there is no constant in "constants" with the same sort.

    • getSatisfactionRatio

      public double getSatisfactionRatio()
      Returns the ratio of worlds not satisfying this formula to worlds satisfying this formula.
      Returns:
      the ratio of worlds not satisfying this formula to worlds satisfying this formula.

    • getUniformProbability

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

    • isGround

      public boolean isGround()
      Checks whether this formula is ground, i.e. whether there appears no variable in this formula.
      Specified by:
      isGround in interface ComplexLogicalFormula
      Returns:
      "true" if this formula is ground.

    • isWellFormed

      public boolean isWellFormed()
      Tests whether this formula is well-formed, i.e. whether
      - there are no two variables with the same name but different sort
      - there are no two constants with the same name but different sort
      - there are no two predicates with the same name but different arguments
      - there are no two functors with the same name but different sort or arguments
      - every atom is complete, i.e. has a complete list of arguments
      - every functional term is complete, i.e. has a complete list of arguments
      - no variable bound by a quantifier is again bound by another quantifier within the first quantifier range.
      - every functor has arity greater zero (otherwise it should be modeled by a constant
      Specified by:
      isWellFormed in interface ComplexLogicalFormula
      Returns:
      "true" if this formula is well-formed

    • containsTermsOfType

      public <C extends Term<?>> boolean containsTermsOfType(Class<C> cls)
      Description copied from interface: LogicStructure
      Checks if this logical structure contains at least one term of type C. This method is a shortcut for !getTerms(TermImplementation.class).isEmpty().
      Specified by:
      containsTermsOfType in interface LogicStructure
      Type Parameters:
      C - the type of terms
      Parameters:
      cls - The class structure representing the type C of the term.
      Returns:
      True if this logical structure contains at least one term of type C or false otherwise.

    • complement

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

    • combineWithOr

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

    • combineWithAnd

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

    • toString

      public abstract String toString()
      Overrides:
      toString in class Object

    • clone

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