Package net.sf.tweety.logics.ml.reasoner
Class SPASSMlReasoner
- java.lang.Object
-
- net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner
-
- net.sf.tweety.logics.ml.reasoner.SPASSMlReasoner
-
- All Implemented Interfaces:
QualitativeReasoner<MlBeliefSet,FolFormula>
,Reasoner<java.lang.Boolean,MlBeliefSet,FolFormula>
public class SPASSMlReasoner extends AbstractMlReasoner
Invokes SPASS (http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/), an automated theorem prover for first-order logic, modal logic and description logics.
Note: There are unresolved errors for some cases, see net.sf.tweety.logics.ml.SPASSTest#ComplexQueryTest() for examples.- Author:
- Anna Gessler, Matthias Thimm
-
-
Field Summary
-
Fields inherited from class net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner
defaultReasoner
-
-
Constructor Summary
Constructors Constructor Description SPASSMlReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific SPASSSPASSMlReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific SPASS Prover.
-
Method Summary
Modifier and Type Method Description java.lang.Boolean
query(MlBeliefSet kb, FolFormula query)
Queries the given belief base for the given formula.java.lang.String
queryProof(MlBeliefSet kb, Formula query)
Determines the answer wrt.void
setCmdOptions(java.lang.String s)
Sets the command line options that will be used by SPASS when executing the query.-
Methods inherited from class net.sf.tweety.logics.ml.reasoner.AbstractMlReasoner
getDefaultReasoner, setDefaultReasoner
-
-
-
-
Constructor Detail
-
SPASSMlReasoner
public SPASSMlReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific SPASS Prover.- Parameters:
binaryLocation
- of the SPASS executable on the hard drivebash
- shell to run commands
-
SPASSMlReasoner
public SPASSMlReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific SPASS- Parameters:
binaryLocation
- of the SPASS executable on the hard drive
-
-
Method Detail
-
setCmdOptions
public void setCmdOptions(java.lang.String s)
Sets the command line options that will be used by SPASS when executing the query.- Parameters:
s
- a string containing the command line arguments
-
query
public java.lang.Boolean query(MlBeliefSet kb, FolFormula query)
Description copied from interface:Reasoner
Queries the given belief base for the given formula.- Specified by:
query
in interfaceQualitativeReasoner<MlBeliefSet,FolFormula>
- Specified by:
query
in interfaceReasoner<java.lang.Boolean,MlBeliefSet,FolFormula>
- Specified by:
query
in classAbstractMlReasoner
- Parameters:
kb
- a belief basequery
- a formula- Returns:
- the answer to the query
-
queryProof
public java.lang.String queryProof(MlBeliefSet kb, Formula query)
Determines the answer wrt. to the given query and returns the proof (if applicable). May decrease SPASS's performance, usequery(MlBeliefSet,FolFormula)
if only a yes/no result is needed.- Parameters:
kb
- a modal belief setquery
- a formula- Returns:
- a string containing proof documentation
-
-