Package org.tweetyproject.logics.pl.analysis

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