Package net.sf.tweety.logics.commons.analysis

Interface InterpolantEnumerator<S extends Formula>

  • Type Parameters:
    S - the type of formulas
    All Known Implementing Classes:
    SimplePlInterpolantEnumerator
    public interface InterpolantEnumerator<S extends Formula>
    Interface for classes enumerating (Craig) interpolants. Given two consistent sets of formulas K1 and K2, an interpolant I of K1 wrt. K2 is a formula with
    • I is entailed by K1
    • I and K2 are inconsistent
    • I only uses vocabulary common to both K1 and K2
    Author:
    Matthias Thimm

    • Method Summary

      Modifier and Type Method Description
      java.util.Collection<S> getInterpolants​(java.util.Collection<S> k1, java.util.Collection<S> k2)
      Returns the set of all interpolants of K1 wrt.
      S getStrongestInterpolant​(java.util.Collection<S> k1, java.util.Collection<S> k2)
      Returns the strongest interpolant (up to semantical equivalence) of K1 wrt.
      S getWeakestInterpolant​(java.util.Collection<S> k1, java.util.Collection<S> k2)
      Returns the weakest interpolant (up to semantical equivalence) of K1 wrt.
      boolean isInterpolant​(S candidate, java.util.Collection<S> k1, java.util.Collection<S> k2)
      Checks whether the given formula "candidate" is an interpolant of k1 wrt.

    • Method Detail

      • getInterpolants

        java.util.Collection<S> getInterpolants​(java.util.Collection<S> k1,
                                        java.util.Collection<S> k2)
        Returns the set of all interpolants of K1 wrt. K2 (modulo semantical equivalence).
        Parameters:
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        the set of all interpolants of K1 wrt. K2 (modulo semantical equivalence).

      • isInterpolant

        boolean isInterpolant​(S candidate,
                      java.util.Collection<S> k1,
                      java.util.Collection<S> k2)
        Checks whether the given formula "candidate" is an interpolant of k1 wrt. k2.
        Parameters:
        candidate - some candidate formula.
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        "true" if "candidate" is an interpolant of k1 wrt. k2.

      • getStrongestInterpolant

        S getStrongestInterpolant​(java.util.Collection<S> k1,
                          java.util.Collection<S> k2)
        Returns the strongest interpolant (up to semantical equivalence) of K1 wrt. K2, i.e., the interpolant IS such that IS entails I for every other interpolant I.
        Parameters:
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        the strongest interpolant of K1 wrt. K2

      • getWeakestInterpolant

        S getWeakestInterpolant​(java.util.Collection<S> k1,
                        java.util.Collection<S> k2)
        Returns the weakest interpolant (up to semantical equivalence) of K1 wrt. K2, i.e., the interpolant IW such that I entails IW for every other interpolant I.
        Parameters:
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        the weakest interpolant of K1 wrt. K2