Class Prover9FolReasoner

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

    • Prover9FolReasoner

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

      public Prover9FolReasoner(String binaryLocation)
      Constructs a new instance pointing to a specific Prover9
      Parameters:
      binaryLocation - of the prover9 executable on the hard drive
  • Method Details

    • 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 Prover9 binaries.
    • setBinaryLocation

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

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