Package org.tweetyproject.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 Details

    • getInterpolants

      Collection<S> getInterpolants(Collection<S> k1, 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, Collection<S> k1, 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(Collection<S> k1, 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(Collection<S> k1, 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