Package net.sf.tweety.logics.ml.reasoner

Class MleanCoPReasoner

java.lang.Object

net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner

net.sf.tweety.logics.ml.reasoner.MleanCoPReasoner

All Implemented Interfaces:

QualitativeReasoner<MlBeliefSet,FolFormula>, Reasoner<java.lang.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

Modifier and Type	Field	Description
private Shell	bash	Shell to run MleanCoP.
private java.lang.String	scriptLocation	String representation of the mleancop.sh path.

Fields inherited from class net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner

defaultReasoner

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
java.lang.String	getScriptLocation()	Get the mleancop.sh path.
java.lang.Boolean	query(MlBeliefSet beliefbase, FolFormula formula)	Queries the given belief base for the given formula.
void	setScriptLocation(java.lang.String location)	Set the mleancop.sh path.

Methods inherited from class net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner

getDefaultReasoner, setDefaultReasoner

Methods inherited from class java.lang.Object

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

Field Detail

scriptLocation

private java.lang.String scriptLocation

String representation of the mleancop.sh path. This shell script specifies the prolog system, prover location and modal logic (D, T, S4 or S5) and domain (constant, cumulative or varying) that will be used.
NOTE: Make sure to set the PROVER_PATH variable in the mleancop.sh script to the location of the mleancop files (= the prolog files).

bash

private Shell bash

Shell to run MleanCoP.

Constructor Detail

MleanCoPReasoner

public MleanCoPReasoner(java.lang.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(java.lang.String location)

Constructs a new instance pointing to a specific MleanCoProver.

Parameters:

location - mleancop.sh path on the hard drive

Method Detail

getScriptLocation

public java.lang.String getScriptLocation()

Get the mleancop.sh path.

Returns:

location of MleanCOP shell script

setScriptLocation

public void setScriptLocation(java.lang.String location)

Set the mleancop.sh path.

Parameters:

location - of MleanCOP shell script

query

public java.lang.Boolean query(MlBeliefSet beliefbase,
                               FolFormula formula)

Description copied from interface: Reasoner

Queries the given belief base for the given formula.

Specified by:

query in interface QualitativeReasoner<MlBeliefSet,FolFormula>

Specified by:

query in interface Reasoner<java.lang.Boolean,MlBeliefSet,FolFormula>

Specified by:

query in class AbstractMlReasoner

Parameters:

beliefbase - a belief base

formula - a formula

Returns:

the answer to the query