Class EFOLReasoner

java.lang.Object
org.tweetyproject.logics.fol.reasoner.FolReasoner
org.tweetyproject.logics.fol.reasoner.EFOLReasoner
All Implemented Interfaces:
QualitativeReasoner<FolBeliefSet,FolFormula>, Reasoner<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
  • Constructor Details

    • EFOLReasoner

      public EFOLReasoner(String binaryLocation, Shell bash)
      Constructs a new instance pointing to a specific EProver.
      Parameters:
      binaryLocation - location of the EProver executable on the hard drive
      bash - shell to run commands
    • EFOLReasoner

      public EFOLReasoner(String binaryLocation)
      Constructs a new instance pointing to a specific EProver.
      Parameters:
      binaryLocation - location of the Eprover executable on the hard drive
  • Method Details

    • setAdditionalArguments

      public void setAdditionalArguments(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 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 Boolean query(FolBeliefSet kb, FolFormula query)
      Description copied from interface: Reasoner
      Queries the given belief base for the given formula.
      Specified by:
      query in interface QualitativeReasoner<FolBeliefSet,FolFormula>
      Specified by:
      query in interface Reasoner<Boolean,FolBeliefSet,FolFormula>
      Specified by:
      query in class FolReasoner
      Parameters:
      kb - a belief base
      query - 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 class FolReasoner
      Parameters:
      kb - the knowledge base
      a - the first formula.
      b - the second formula.
      Returns:
      the answer to the query.
    • getBinaryLocation

      public String getBinaryLocation()
      Returns:
      the path of the EProver binary
    • setBinaryLocation

      public void setBinaryLocation(String binaryLocation)
      Changes the path of the EProver binary.
      Parameters:
      binaryLocation - the new path of the EProver binary
    • isInstalled

      public boolean isInstalled()
      Returns:
      if the solver is installed