Class SimplePlInterpolantEnumerator
java.lang.Object
org.tweetyproject.logics.pl.analysis.SimplePlInterpolantEnumerator
- All Implemented Interfaces:
InterpolantEnumerator<PlFormula>
public class SimplePlInterpolantEnumerator
extends Object
implements InterpolantEnumerator<PlFormula>
Implements an exhaustive search approach to compute all interpolants of
a knowledge base wrt. another knowledge base.
- Author:
- Matthias Thimm
-
Constructor Summary
ConstructorDescriptionSimplePlInterpolantEnumerator(AbstractPlReasoner reasoner)
Creates a new SimplePlInterpolantEnumerator that uses the given PL reasoner for entailment queries. -
Method Summary
Modifier and TypeMethodDescriptiongetInterpolants(Collection<PlFormula> k1, Collection<PlFormula> k2)
Returns the set of all interpolants of K1 wrt.Returns the strongest interpolant (up to semantical equivalence) of K1 wrt.getWeakestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)
Returns the weakest interpolant (up to semantical equivalence) of K1 wrt.boolean
isInterpolant(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2)
Checks whether the given formula "candidate" is an interpolant of k1 wrt.
-
Constructor Details
-
SimplePlInterpolantEnumerator
Creates a new SimplePlInterpolantEnumerator that uses the given PL reasoner for entailment queries.- Parameters:
reasoner
- some PL reasoner
-
-
Method Details
-
getInterpolants
Description copied from interface:InterpolantEnumerator
Returns the set of all interpolants of K1 wrt. K2 (modulo semantical equivalence).- Specified by:
getInterpolants
in interfaceInterpolantEnumerator<PlFormula>
- Parameters:
k1
- some set of formulask2
- some set of formulas- Returns:
- the set of all interpolants of K1 wrt. K2 (modulo semantical equivalence).
-
isInterpolant
public boolean isInterpolant(PlFormula candidate, Collection<PlFormula> k1, 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 interfaceInterpolantEnumerator<PlFormula>
- Parameters:
candidate
- some candidate formula.k1
- some set of formulask2
- some set of formulas- Returns:
- "true" if "candidate" is an interpolant of k1 wrt. k2.
-
getStrongestInterpolant
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 interfaceInterpolantEnumerator<PlFormula>
- Parameters:
k1
- some set of formulask2
- some set of formulas- Returns:
- the strongest interpolant of K1 wrt. K2
-
getWeakestInterpolant
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 interfaceInterpolantEnumerator<PlFormula>
- Parameters:
k1
- some set of formulask2
- some set of formulas- Returns:
- the weakest interpolant of K1 wrt. K2
-