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 Summary

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

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