Class SpassFolReasoner
- java.lang.Object
-
- net.sf.tweety.logics.fol.reasoner.FolReasoner
-
- net.sf.tweety.logics.fol.reasoner.SpassFolReasoner
-
- All Implemented Interfaces:
QualitativeReasoner<FolBeliefSet,FolFormula>
,Reasoner<java.lang.Boolean,FolBeliefSet,FolFormula>
public class SpassFolReasoner extends FolReasoner
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.- Author:
- Anna Gessler
-
-
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.fol.reasoner.FolReasoner
defaultReasoner
-
-
Constructor Summary
Constructors Constructor Description SpassFolReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific SPASSSpassFolReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific SPASS Prover.
-
Method Summary
Modifier and Type Method Description boolean
equivalent(FolBeliefSet kb, FolFormula a, FolFormula b)
This method determines whether two formulas are equivalent wrt.private boolean
evaluateResult(java.lang.String output)
Evaluates SPASS results.java.lang.Boolean
query(FolBeliefSet kb, FolFormula query)
Queries the given belief base for the given formula.java.lang.String
queryProof(FolBeliefSet 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.fol.reasoner.FolReasoner
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
-
SpassFolReasoner
public SpassFolReasoner(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
-
SpassFolReasoner
public SpassFolReasoner(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(FolBeliefSet kb, FolFormula query)
Description copied from interface:Reasoner
Queries the given belief base for the given formula.- Specified by:
query
in interfaceQualitativeReasoner<FolBeliefSet,FolFormula>
- Specified by:
query
in interfaceReasoner<java.lang.Boolean,FolBeliefSet,FolFormula>
- Specified by:
query
in classFolReasoner
- Parameters:
kb
- a belief basequery
- a formula- Returns:
- the answer to the query
-
queryProof
public java.lang.String queryProof(FolBeliefSet kb, Formula query)
Determines the answer wrt. to the given query and returns the proof (if applicable). May decrease SPASS's performance, usequery(FolBeliefSet,FolFormula)
if only a yes/no result is needed.- Parameters:
kb
- the knowledge basequery
- 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
-
equivalent
public boolean equivalent(FolBeliefSet kb, FolFormula a, FolFormula b)
Description copied from class:FolReasoner
This method determines whether two formulas are equivalent wrt. to the given knowledge base.- Specified by:
equivalent
in classFolReasoner
- Parameters:
kb
- the knowledge basea
- the first formula.b
- the second formula.- Returns:
- the answer to the query.
-
-