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 Link icon

    • RelationalFormula Link icon

      public RelationalFormula()

  • Method Details Link icon

    • getFormula Link icon

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

    • getAtoms Link icon

      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 Link icon

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

    • getPredicateCls Link icon

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

    • substitute Link icon

      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 Link icon

      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 Link icon

      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 Link icon

      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 Link icon

      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 Link icon

      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 Link icon

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

    • isGround Link icon

      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 Link icon

      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 Link icon

      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 Link icon

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

    • combineWithOr Link icon

      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 Link icon

      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 Link icon

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

    • clone Link icon

      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