Class ExclusiveDisjunction

All Implemented Interfaces:
Iterable<PlFormula>, Collection<PlFormula>, List<PlFormula>, Formula, AssociativeFormulaSupport.AssociativeSupportBridge, AssociativeFormula<PlFormula>, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

public class ExclusiveDisjunction extends AssociativePlFormula
This class represents an exclusive disjunction (XOR) in propositional logic.
Author:
Anna Gessler, Matthias Thimm
  • Constructor Details

    • ExclusiveDisjunction

      public ExclusiveDisjunction(Collection<? extends PlFormula> formulas)
      Creates a new XOR formula with the given inner formulas.
      Parameters:
      formulas - a collection of formulas.
    • ExclusiveDisjunction

      public ExclusiveDisjunction()
      Creates a new (empty) exclusive disjunction.
    • ExclusiveDisjunction

      public ExclusiveDisjunction(PlFormula first, PlFormula second)
      Creates a new exclusive disjunction with the two given formulae
      Parameters:
      first - a propositional formula.
      second - a propositional formula.
  • Method Details

    • collapseAssociativeFormulas

      public PlFormula collapseAssociativeFormulas()
      Description copied from class: PlFormula
      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 PlFormula
      Returns:
      the collapsed formula.
    • toNnf

      public PlFormula toNnf()
      Description copied from class: PlFormula
      This method returns this formula in negation normal form (NNF). A formula is in NNF iff negations occur only directly in front of a proposition.
      Specified by:
      toNnf in class PlFormula
      Returns:
      the formula in NNF.
    • clone

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

      public ExclusiveDisjunction 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
    • toCnf

      public Conjunction toCnf()
      Description copied from class: PlFormula
      This method returns this formula in conjunctive normal form (CNF). A formula is in CNF iff it is a conjunction of disjunctions and in NNF. The CNF generated by this method is not necessarily minimal.
      Specified by:
      toCnf in class PlFormula
      Returns:
      the formula in CNF.
    • trim

      public PlFormula trim()
      Description copied from class: PlFormula
      Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies.
      Specified by:
      trim in class PlFormula
      Returns:
      an equivalent formula without duplicates.
    • getModels

      public Set<PossibleWorld> getModels(PlSignature sig)
      Description copied from class: PlFormula
      Returns the set of models of this formula wrt. the given signature.
      Specified by:
      getModels in class PlFormula
      Parameters:
      sig - some propositional signature
      Returns:
      the set of models of this formula wrt. the given signature.
    • isClause

      public boolean isClause()
      Description copied from class: PlFormula
      Checks whether this formula is a clause, i.e. whether it is a disjunction of literals.
      Overrides:
      isClause in class PlFormula
      Returns:
      "true" iff this formula is a clause.
    • replace

      public PlFormula replace(Proposition p, PlFormula f, int i)
      Description copied from class: PlFormula
      Replaces the ith instance of the proposition p by f.
      Specified by:
      replace in class PlFormula
      Parameters:
      p - some proposition
      f - some formula
      i - the index of the proposition
      Returns:
      a new formula with the ith instance of the proposition p replaced by f.