Package org.tweetyproject.logics.ml.reasoner

Class MleanCoPReasoner

java.lang.Object

org.tweetyproject.logics.ml.reasoner.AbstractMlReasoner

org.tweetyproject.logics.ml.reasoner.MleanCoPReasoner

All Implemented Interfaces:

QualitativeReasoner<MlBeliefSet,FolFormula>, Reasoner<Boolean,MlBeliefSet,FolFormula>

public class MleanCoPReasoner
extends AbstractMlReasoner

Invokes MleanCoP (http://www.leancop.de/mleancop/), a compact automated theorem prover for modal first-order logic based on the clausal connection calculus. It checks whether a given formula is valid.
NOTE: Make sure to set the PROVER_PATH variable in the mleancop.sh script to the location of the mleancop files (= the Prolog files).

Author:

Anna Gessler, Matthias Thimm

Field Summary

Fields inherited from class org.tweetyproject.logics.ml.reasoner.AbstractMlReasoner

defaultReasoner

Constructor Summary

Constructors

Constructor	Description
MleanCoPReasoner(String location)	Constructs a new instance pointing to a specific MleanCoProver.
MleanCoPReasoner(String location, Shell bash)	Constructs a new instance pointing to a specific MleanCoProver.

Method Summary

Modifier and Type	Method	Description
String	getScriptLocation()	Get the mleancop.sh path.
boolean	isInstalled()	Checks whether the underlying solver or reasoning mechanism used by this reasoner is installed and available for use.
Boolean	query(MlBeliefSet beliefbase, FolFormula formula)	Queries the given belief base with the provided formula and returns a boolean result.
void	setScriptLocation(String location)	Set the mleancop.sh path.

Methods inherited from class org.tweetyproject.logics.ml.reasoner.AbstractMlReasoner

getDefaultReasoner, setDefaultReasoner

Methods inherited from class java.lang.Object

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

Constructor Details

MleanCoPReasoner

public MleanCoPReasoner(String location,
 Shell bash)

Constructs a new instance pointing to a specific MleanCoProver.

Parameters:

location - mleancop.sh path on the hard drive

bash - shell to run commands

MleanCoPReasoner

public MleanCoPReasoner(String location)

Constructs a new instance pointing to a specific MleanCoProver.

Parameters:

location - mleancop.sh path on the hard drive

Method Details

getScriptLocation

public String getScriptLocation()

Get the mleancop.sh path.

Returns:

location of MleanCOP shell script

setScriptLocation

public void setScriptLocation(String location)

Set the mleancop.sh path.

Parameters:

location - of MleanCOP shell script

query

public Boolean query(MlBeliefSet beliefbase,
 FolFormula formula)

Description copied from interface: QualitativeReasoner

Queries the given belief base with the provided formula and returns a boolean result. The result indicates whether the formula is entailed or satisfied by the belief base according to the qualitative reasoning method implemented by the reasoner.

Specified by:

query in interface QualitativeReasoner<MlBeliefSet,FolFormula>

Specified by:

query in interface Reasoner<Boolean,MlBeliefSet,FolFormula>

Specified by:

query in class AbstractMlReasoner

Parameters:

beliefbase - The belief base to be queried.

formula - The formula for which the query is made.

Returns:

`TRUE` if the formula is entailed or satisfied by the belief base, `FALSE` otherwise.

isInstalled

public boolean isInstalled()

Description copied from interface: QualitativeReasoner

Checks whether the underlying solver or reasoning mechanism used by this reasoner is installed and available for use. This can be helpful when the reasoner depends on external tools or libraries for performing the reasoning tasks.

Returns:

`true` if the solver is installed and available, `false` otherwise.