Package net.sf.tweety.logics.pl.analysis
Class SimplePlInterpolantEnumerator
- java.lang.Object
-
- net.sf.tweety.logics.pl.analysis.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
-
-
Constructor Summary
Constructors Constructor Description SimplePlInterpolantEnumerator(AbstractPlReasoner reasoner)
Creates a new SimplePlInterpolantEnumerator that uses the given PL reasoner for entailment queries.
-
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.
-
-
-
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 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, 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 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
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 interfaceInterpolantEnumerator<PlFormula>
- Parameters:
k1
- some set of formulask2
- 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 interfaceInterpolantEnumerator<PlFormula>
- Parameters:
k1
- some set of formulask2
- some set of formulas- Returns:
- the weakest interpolant of K1 wrt. K2
-
-