Class Prover9FolReasoner
- java.lang.Object
-
- net.sf.tweety.logics.fol.reasoner.FolReasoner
-
- net.sf.tweety.logics.fol.reasoner.Prover9FolReasoner
-
- All Implemented Interfaces:
QualitativeReasoner<FolBeliefSet,FolFormula>
,Reasoner<java.lang.Boolean,FolBeliefSet,FolFormula>
public class Prover9FolReasoner extends FolReasoner
Invokes Prover9 ( https://www.cs.unm.edu/~mccune/mace4/), an automated theorem prover for first-order logic, and returns its results.- Author:
- Nils Geilen, Matthias Thimm
-
-
Field Summary
Fields Modifier and Type Field Description private Shell
bash
Shell to run Prover9private java.lang.String
binaryLocation
String representation of the EProver binary path.-
Fields inherited from class net.sf.tweety.logics.fol.reasoner.FolReasoner
defaultReasoner
-
-
Constructor Summary
Constructors Constructor Description Prover9FolReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific Prover9Prover9FolReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific Prover9.
-
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
eval(java.io.File file)
Invokes Prover9.java.lang.String
getBinaryLocation()
Returns the path of the Prover9 binaries.java.lang.Boolean
query(FolBeliefSet kb, FolFormula query)
Queries the given belief base for the given formula.void
setBinaryLocation(java.lang.String binaryLocation)
Changes the path of the Prover9 binaries.-
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 EProver binary path. Temporary files are stored in this directory.
-
bash
private Shell bash
Shell to run Prover9
-
-
Constructor Detail
-
Prover9FolReasoner
public Prover9FolReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific Prover9.- Parameters:
binaryLocation
- of the prover9 executable on the hard drivebash
- shell to run commands
-
Prover9FolReasoner
public Prover9FolReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific Prover9- Parameters:
binaryLocation
- of the prover9 executable on the hard drive
-
-
Method Detail
-
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
-
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.
-
eval
private boolean eval(java.io.File file) throws java.lang.Exception
Invokes Prover9.- Parameters:
file
- input file for Prover9- Returns:
- query result
- Throws:
java.lang.Exception
- if something goes wrong
-
getBinaryLocation
public java.lang.String getBinaryLocation()
Returns the path of the Prover9 binaries.- Returns:
- binary location of Prover9
-
setBinaryLocation
public void setBinaryLocation(java.lang.String binaryLocation)
Changes the path of the Prover9 binaries.- Parameters:
binaryLocation
- the new path of the binary
-
-