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