Class Conjunction

java.lang.Object
org.tweetyproject.logics.commons.syntax.RelationalFormula
org.tweetyproject.logics.fol.syntax.FolFormula
org.tweetyproject.logics.fol.syntax.AssociativeFolFormula
org.tweetyproject.logics.fol.syntax.Conjunction
All Implemented Interfaces:
Iterable<RelationalFormula>, Collection<RelationalFormula>, List<RelationalFormula>, SequencedCollection<RelationalFormula>, Formula, AssociativeFormulaSupport.AssociativeSupportBridge, AssociativeFormula<RelationalFormula>, ClassicalFormula, ComplexLogicalFormula, Conjunctable, Disjunctable, Invertable, LogicStructure, ProbabilityAware, QuantifiedFormula, SimpleLogicalFormula
public class Conjunction extends AssociativeFolFormula
The classical conjunction of first-order logic.
Author:
Matthias Thimm

  • Constructor Details

    • Conjunction

      public Conjunction(Collection<? extends RelationalFormula> formulas)
      Creates a new conjunction with the given inner formulas.
      Parameters:
      formulas - a collection of formulas.

    • Conjunction

      public Conjunction()
      Creates a new (empty) conjunction.

    • Conjunction

      public Conjunction(RelationalFormula first, RelationalFormula second)
      Creates a new conjunction with the two given formulae
      Parameters:
      first - a relational formula.
      second - a relational formula.

  • Method Details

    • isDnf

      public boolean isDnf()
      Description copied from class: FolFormula
      Checks whether this formula is in disjunctive normal form.
      Specified by:
      isDnf in class FolFormula
      Returns:
      "true" iff this formula is in disjunctive normal form.

    • substitute

      public Conjunction 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
      Overrides:
      substitute in class AssociativeFolFormula
      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).

    • toNnf

      public FolFormula toNnf()
      Description copied from class: FolFormula
      Makes the negation normal form of this formula.
      Specified by:
      toNnf in class FolFormula
      Returns:
      the NNF of this formula

    • 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
      Returns:
      the collapsed formula.

    • clone

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

    • createEmptyFormula

      public Conjunction createEmptyFormula()
      Returns:
      an empty version of the AssociativeFormula

    • getOperatorSymbol

      public String getOperatorSymbol()
      Returns:
      A String representing the operator which connects two items of the associative formula.

    • getEmptySymbol

      public String getEmptySymbol()
      Returns:
      A String representing an empty version of the Associative Formula implementation