Package org.tweetyproject.logics.ml.reasoner

Class SPASSMlReasoner

java.lang.Object
org.tweetyproject.logics.ml.reasoner.AbstractMlReasoner
org.tweetyproject.logics.ml.reasoner.SPASSMlReasoner
All Implemented Interfaces:
QualitativeReasoner<MlBeliefSet,FolFormula>, Reasoner<Boolean,MlBeliefSet,FolFormula>
public class SPASSMlReasoner extends AbstractMlReasoner
Invokes SPASS (http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/), an automated theorem prover for first-order logic, modal logic and description logics.
Note: There are unresolved errors for some cases, see org.tweetyproject.logics.ml.SPASSTest#ComplexQueryTest() for examples.
Author:
Anna Gessler, Matthias Thimm

  • Constructor Details

    • SPASSMlReasoner

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

    • SPASSMlReasoner

      public SPASSMlReasoner(String binaryLocation)
      Constructs a new instance pointing to a specific SPASS
      Parameters:
      binaryLocation - of the SPASS executable on the hard drive

  • Method Details

    • setCmdOptions

      public void setCmdOptions(String s)
      Sets the command line options that will be used by SPASS when executing the query.
      Parameters:
      s - a string containing the command line arguments

    • query

      public Boolean query(MlBeliefSet kb, FolFormula query)
      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:
      kb - a belief base
      query - a formula
      Returns:
      the answer to the query

    • queryProof

      public String queryProof(MlBeliefSet kb, Formula query)
      Determines the answer wrt. to the given query and returns the proof (if applicable). May decrease SPASS's performance, use query(MlBeliefSet,FolFormula) if only a yes/no result is needed.
      Parameters:
      kb - a modal belief set
      query - a formula
      Returns:
      a string containing proof documentation

    • isInstalled

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