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