Class Disjunction

    • Constructor Detail

      • Disjunction

        public Disjunction​(java.util.Collection<? extends PlFormula> formulas)
        Creates a new disjunction with the given inner formulas.
        Parameters:
        formulas - a collection of formulas.
      • Disjunction

        public Disjunction()
        Creates a new (empty) disjunction.
      • Disjunction

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

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

        public Disjunction createEmptyFormula()
        Returns:
        an empty version of the AssociativeFormula
      • getOperatorSymbol

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

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