Package org.tweetyproject.logics.pl.syntax

Class PlFormula

    • Constructor Detail

      • PlFormula

        public PlFormula()

    • Method Detail

      • 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.

      • getLiterals

        public abstract java.util.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.

      • 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.

      • 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 java.util.Collection<PlFormula> getPrimeImplicants()
        Returns the set of prime implicants of this formula.
        Returns:
        the set of prime implicants of this formula.

      • getModels

        public java.util.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 java.util.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.

      • 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​(java.lang.Object other)
        Specified by:
        equals in interface SimpleLogicalFormula
        Overrides:
        equals in class java.lang.Object

      • hashCode

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