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 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.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
-
-
-
-
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
-
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.
-
-