Package org.tweetyproject.logics.pl.analysis

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

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
Collection<PlFormula>	getInterpolants(Collection<PlFormula> k1, Collection<PlFormula> k2)	Returns the set of all interpolants of K1 wrt.
PlFormula	getStrongestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)	Returns the strongest interpolant (up to semantical equivalence) of K1 wrt.
PlFormula	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.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

SimplePlInterpolantEnumerator

public SimplePlInterpolantEnumerator(AbstractPlReasoner reasoner)

Creates a new SimplePlInterpolantEnumerator that uses the given PL reasoner for entailment queries.

Parameters:

reasoner - some PL reasoner

Method Details

getInterpolants

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