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 Modifier and Type Field Description private Shell
bash
Shell to run SPASS.private java.lang.String
binaryLocation
String representation of the SPASS path.private java.lang.String
cmdOptions
Command line options that will be used by SPASS when executing the query.-
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 private boolean
evaluateResult(java.lang.String output)
Evaluates SPASS results.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
-
-
-
-
Field Detail
-
binaryLocation
private java.lang.String binaryLocation
String representation of the SPASS path.
-
bash
private Shell bash
Shell to run SPASS.
-
cmdOptions
private java.lang.String cmdOptions
Command line options that will be used by SPASS when executing the query. The default value disables most outputs except for the result and enables TPTP input format instead of SPASS input format.
-
-
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
-
evaluateResult
private boolean evaluateResult(java.lang.String output)
Evaluates SPASS results.- Parameters:
output
- of a SPASS query- Returns:
- true if a proof was found, false otherwise
-
-