Class PlFormula

java.lang.Object
org.tweetyproject.logics.pl.syntax.PlFormula
All Implemented Interfaces:
Formula, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula
Direct Known Subclasses:
AssociativePlFormula, Equivalence, ExistsQuantifiedFormula, ForallQuantifiedFormula, Implication, Indecision, Negation, Proposition, SpecialFormula, WeakNegation
public abstract class PlFormula extends Object implements ClassicalFormula
This class represents the common ancestor for propositional formulae.
Author:
Matthias Thimm, Tim Janus

  • Constructor Details

    • PlFormula

      public PlFormula()
      Default Constructor

  • Method Details

    • getPredicateCls

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

    • getSignature

      public PlSignature getSignature()
      Description copied from interface: Formula
      Returns the signature of the language of this formula.
      Specified by:
      getSignature in interface Formula
      Returns:
      the signature of the language of this formula.

    • getAtoms

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

    • getLiterals

      public abstract Set<PlFormula> getLiterals()
      Returns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.
      Returns:
      all literals appearing in this formula.

    • 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
      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
      Parameters:
      f - a formula to be combined with OR and this.
      Returns:
      a disjunction of this and the given formula.

    • collapseAssociativeFormulas

      public abstract PlFormula 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.

    • getPredicates

      public abstract Set<PlPredicate> getPredicates()
      Description copied from interface: SimpleLogicalFormula
      Processes the set of all predicates which appear in this formula
      Specified by:
      getPredicates in interface SimpleLogicalFormula
      Returns:
      all predicates that appear in this formula

    • trim

      public abstract PlFormula trim()
      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.
      Returns:
      an equivalent formula without duplicates.

    • getUniformProbability

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

    • toNnf

      public abstract PlFormula toNnf()
      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.
      Returns:
      the formula in NNF.

    • toCnf

      public abstract Conjunction toCnf()
      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.
      Returns:
      the formula in CNF.

    • toDnf

      public PlFormula toDnf()
      This method returns this formula in disjunctive normal form (DNF). A formula is in DNF iff it is a disjunction of conjunctive clauses. The DNF generated by this method is not necessarily minimal.
      Returns:
      the formula in DNF.

    • resolvableWith

      public boolean resolvableWith(PlFormula other)
      Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formula (which is also a conjunction of literals), i.e. whether they contains exactly one complementary literal.
      Parameters:
      other - a conjunction of literals
      Returns:
      "true" iff this formula is resolvable with the other formula.

    • resolveWith

      public Conjunction resolveWith(PlFormula other)
      Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.
      Parameters:
      other - a conjunction of formulas
      Returns:
      some resolvent.

    • toBlakeCanonicalForm

      public PlFormula toBlakeCanonicalForm()
      This method returns this formula in Blake canonical form. A formula is in Blake canonical form iff it is the disjunction of its prime implicants.
      Returns:
      the formula in Blake canonical form

    • getPrimeImplicants

      public Collection<PlFormula> getPrimeImplicants()
      Returns the set of prime implicants of this formula.
      Returns:
      the set of prime implicants of this formula.

    • getModels

      public Set<PossibleWorld> getModels()
      Returns the set of models of this formula wrt. a signature that only contains the propositions appearing in this formula.
      Returns:
      the set of models of this formula wrt. a signature that only contains the propositions appearing in this formula.

    • getModels

      public abstract Set<PossibleWorld> getModels(PlSignature sig)
      Returns the set of models of this formula wrt. the given signature.
      Parameters:
      sig - some propositional signature
      Returns:
      the set of models of this formula wrt. the given signature.

    • complement

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

    • isClause

      public boolean isClause()
      Checks whether this formula is a clause, i.e. whether it is a disjunction of literals.
      Returns:
      "true" iff this formula is a clause.

    • isConjunctiveClause

      public boolean isConjunctiveClause()
      Checks whether this formula is a conjunctive clause, i.e. whether it is a conjunction of literals.
      Returns:
      "true" iff this formula is a conjunctive clause.

    • numberOfOccurrences

      public abstract int numberOfOccurrences(Proposition p)
      Returns the number of occurrences of the given proposition within this formula
      Parameters:
      p - some proposition
      Returns:
      the number of occurrences of the given proposition within this formula

    • replace

      public abstract PlFormula replace(Proposition p, PlFormula f, int i)
      Replaces the ith instance of the proposition p by f.
      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.

    • isLiteral

      public boolean isLiteral()
      Specified by:
      isLiteral in interface SimpleLogicalFormula
      Returns:
      true if the formula represents a literal in the language or false otherwise

    • equals

      public abstract boolean equals(Object other)
      Specified by:
      equals in interface SimpleLogicalFormula
      Overrides:
      equals in class Object

    • hashCode

      public abstract int hashCode()
      Specified by:
      hashCode in interface SimpleLogicalFormula
      Overrides:
      hashCode in class Object

    • clone

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