Class EFOLReasoner
- java.lang.Object
-
- net.sf.tweety.logics.fol.reasoner.FolReasoner
-
- net.sf.tweety.logics.fol.reasoner.EFOLReasoner
-
- All Implemented Interfaces:
QualitativeReasoner<FolBeliefSet,FolFormula>
,Reasoner<java.lang.Boolean,FolBeliefSet,FolFormula>
public class EFOLReasoner extends FolReasoner
Invokes E (http://eprover.org), an automated theorem prover for first-order logic, and returns its results.- Author:
- Bastian Wolf, Nils Geilen, Matthias Thimm
-
-
Field Summary
Fields Modifier and Type Field Description private java.lang.String
additionalArguments
Additional arguments for the call to the EProver binary (Default value is "--auto-schedule" which seems to be working best in general)private Shell
bash
Shell to run EProverprivate 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 EFOLReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific EProver.EFOLReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific EProver.
-
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
getAdditionalArguments()
Returns the additional arguments given to the call of the EProver binary (Default value is "--auto-schedule").java.lang.String
getBinaryLocation()
Returns the path of the EProver binary.java.lang.Boolean
query(FolBeliefSet kb, FolFormula query)
Queries the given belief base for the given formula.void
setAdditionalArguments(java.lang.String s)
Sets the additional arguments given to the call of the EProver binary (Default value is "--auto-schedule").void
setBinaryLocation(java.lang.String binaryLocation)
Changes the path of the EProver binary.-
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.
-
additionalArguments
private java.lang.String additionalArguments
Additional arguments for the call to the EProver binary (Default value is "--auto-schedule" which seems to be working best in general)
-
bash
private Shell bash
Shell to run EProver
-
-
Constructor Detail
-
EFOLReasoner
public EFOLReasoner(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific EProver.- Parameters:
binaryLocation
- location of the EProver executable on the hard drivebash
- shell to run commands
-
EFOLReasoner
public EFOLReasoner(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific EProver.- Parameters:
binaryLocation
- location of the Eprover executable on the hard drive
-
-
Method Detail
-
setAdditionalArguments
public void setAdditionalArguments(java.lang.String s)
Sets the additional arguments given to the call of the EProver binary (Default value is "--auto-schedule").- Parameters:
s
- some string
-
getAdditionalArguments
public java.lang.String getAdditionalArguments()
Returns the additional arguments given to the call of the EProver binary (Default value is "--auto-schedule").- Returns:
- the additional 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
-
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 EProver binary.- Returns:
- the path of the EProver binary
-
setBinaryLocation
public void setBinaryLocation(java.lang.String binaryLocation)
Changes the path of the EProver binary.- Parameters:
binaryLocation
- the new path of the EProver binary
-
-