Class SimplePlInterpolantEnumerator

  • All Implemented Interfaces:
    InterpolantEnumerator<PlFormula>

    public class SimplePlInterpolantEnumerator
    extends java.lang.Object
    implements InterpolantEnumerator<PlFormula>
    Implements an exhaustive search approach to compute all interpolants of a knowledge base wrt. another knowledge base.
    Author:
    Matthias Thimm
    • Method Summary

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

        equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • SimplePlInterpolantEnumerator

        public SimplePlInterpolantEnumerator​(AbstractPlReasoner reasoner)
        Creates a new SimplePlInterpolantEnumerator that uses the given PL reasoner for entailment queries.
        Parameters:
        reasoner - some PL reasoner
    • Method Detail

      • getInterpolants

        public java.util.Collection<PlFormula> getInterpolants​(java.util.Collection<PlFormula> k1,
                                                               java.util.Collection<PlFormula> k2)
        Description copied from interface: InterpolantEnumerator
        Returns the set of all interpolants of K1 wrt. K2 (modulo semantical equivalence).
        Specified by:
        getInterpolants in interface InterpolantEnumerator<PlFormula>
        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

        public boolean isInterpolant​(PlFormula candidate,
                                     java.util.Collection<PlFormula> k1,
                                     java.util.Collection<PlFormula> k2)
        Description copied from interface: InterpolantEnumerator
        Checks whether the given formula "candidate" is an interpolant of k1 wrt. k2.
        Specified by:
        isInterpolant in interface InterpolantEnumerator<PlFormula>
        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

        public PlFormula getStrongestInterpolant​(java.util.Collection<PlFormula> k1,
                                                 java.util.Collection<PlFormula> k2)
        Description copied from interface: InterpolantEnumerator
        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.
        Specified by:
        getStrongestInterpolant in interface InterpolantEnumerator<PlFormula>
        Parameters:
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        the strongest interpolant of K1 wrt. K2
      • getWeakestInterpolant

        public PlFormula getWeakestInterpolant​(java.util.Collection<PlFormula> k1,
                                               java.util.Collection<PlFormula> k2)
        Description copied from interface: InterpolantEnumerator
        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.
        Specified by:
        getWeakestInterpolant in interface InterpolantEnumerator<PlFormula>
        Parameters:
        k1 - some set of formulas
        k2 - some set of formulas
        Returns:
        the weakest interpolant of K1 wrt. K2