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: QualitativeReasoner
      Queries the given belief base with the provided formula and returns a boolean result. The result indicates whether the formula is entailed or satisfied by the belief base according to the qualitative reasoning method implemented by the reasoner.
      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 - The belief base to be queried.
      formula - The formula for which the query is made.
      Returns:
      `TRUE` if the formula is entailed or satisfied by the belief base, `FALSE` otherwise.

    • isInstalled

      public boolean isInstalled()
      Description copied from interface: QualitativeReasoner
      Checks whether the underlying solver or reasoning mechanism used by this reasoner is installed and available for use. This can be helpful when the reasoner depends on external tools or libraries for performing the reasoning tasks.
      Returns:
      `true` if the solver is installed and available, `false` otherwise.