Class MleanCoPReasoner

java.lang.Object
org.tweetyproject.logics.ml.reasoner.AbstractMlReasoner
org.tweetyproject.logics.ml.reasoner.MleanCoPReasoner
All Implemented Interfaces:
QualitativeReasoner<MlBeliefSet,FolFormula>, Reasoner<Boolean,MlBeliefSet,FolFormula>

public class MleanCoPReasoner extends AbstractMlReasoner
Invokes MleanCoP (http://www.leancop.de/mleancop/), a compact automated theorem prover for modal first-order logic based on the clausal connection calculus. It checks whether a given formula is valid.
NOTE: Make sure to set the PROVER_PATH variable in the mleancop.sh script to the location of the mleancop files (= the Prolog files).
Author:
Anna Gessler, Matthias Thimm
  • Constructor Details

    • MleanCoPReasoner

      public MleanCoPReasoner(String location, Shell bash)
      Constructs a new instance pointing to a specific MleanCoProver.
      Parameters:
      location - mleancop.sh path on the hard drive
      bash - shell to run commands
    • MleanCoPReasoner

      public MleanCoPReasoner(String location)
      Constructs a new instance pointing to a specific MleanCoProver.
      Parameters:
      location - mleancop.sh path on the hard drive
  • Method Details

    • getScriptLocation

      public String getScriptLocation()
      Get the mleancop.sh path.
      Returns:
      location of MleanCOP shell script
    • setScriptLocation

      public void setScriptLocation(String location)
      Set the mleancop.sh path.
      Parameters:
      location - of MleanCOP shell script
    • query

      public Boolean query(MlBeliefSet beliefbase, FolFormula formula)
      Description copied from interface: Reasoner
      Queries the given belief base for the given formula.
      Specified by:
      query in interface QualitativeReasoner<MlBeliefSet,FolFormula>
      Specified by:
      query in interface Reasoner<Boolean,MlBeliefSet,FolFormula>
      Specified by:
      query in class AbstractMlReasoner
      Parameters:
      beliefbase - a belief base
      formula - a formula
      Returns:
      the answer to the query
    • isInstalled

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