Interface ComplexLogicalFormula

    • Method Detail

      • substitute

        ComplexLogicalFormula substitute​(Term<?> v,
                                         Term<?> t)
                                  throws java.lang.IllegalArgumentException
        Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.
        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:
        java.lang.IllegalArgumentException - if "v" and "t" are of different sorts
      • substitute

        ComplexLogicalFormula substitute​(java.util.Map<? extends Term<?>,​? extends Term<?>> map)
                                  throws java.lang.IllegalArgumentException
        Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
        Parameters:
        map - a mapping defining which terms to be substituted.
        Returns:
        a formula where every term in map.keyset() has been replaced by map.get(v).
        Throws:
        java.lang.IllegalArgumentException - if any term and its mapping are of different sorts
      • exchange

        ComplexLogicalFormula exchange​(Term<?> v,
                                       Term<?> t)
                                throws java.lang.IllegalArgumentException
        Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula.
        Parameters:
        v - a term.
        t - a term.
        Returns:
        a new logical formula with both "v" and "t" exchanged.
        Throws:
        java.lang.IllegalArgumentException - if "v" and "t" are of different sorts
      • isGround

        boolean isGround()
        Checks whether this formula is ground, i.e. whether there appears no variable in this formula.
        Returns:
        "true" if this formula is ground.
      • isWellFormed

        boolean isWellFormed()
        Checks if this formula is well formed in the logical langauge. What well- formed means is highly language dependent and the documentation of implementing sub classes shall describe the well formed term for the language they model.
        Returns:
        true if the formula is well-formed, false otherwise