Class SPASSMlReasoner

    • Field Summary

      Fields 
      Modifier and Type Field Description
      private Shell bash
      Shell to run SPASS.
      private java.lang.String binaryLocation
      String representation of the SPASS path.
      private java.lang.String cmdOptions
      Command line options that will be used by SPASS when executing the query.
    • Constructor Summary

      Constructors 
      Constructor Description
      SPASSMlReasoner​(java.lang.String binaryLocation)
      Constructs a new instance pointing to a specific SPASS
      SPASSMlReasoner​(java.lang.String binaryLocation, Shell bash)
      Constructs a new instance pointing to a specific SPASS Prover.
    • Method Summary

      Modifier and Type Method Description
      private boolean evaluateResult​(java.lang.String output)
      Evaluates SPASS results.
      java.lang.Boolean query​(MlBeliefSet kb, FolFormula query)
      Queries the given belief base for the given formula.
      java.lang.String queryProof​(MlBeliefSet kb, Formula query)
      Determines the answer wrt.
      void setCmdOptions​(java.lang.String s)
      Sets the command line options that will be used by SPASS when executing the query.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • binaryLocation

        private java.lang.String binaryLocation
        String representation of the SPASS path.
      • bash

        private Shell bash
        Shell to run SPASS.
      • cmdOptions

        private java.lang.String cmdOptions
        Command line options that will be used by SPASS when executing the query. The default value disables most outputs except for the result and enables TPTP input format instead of SPASS input format.
    • Constructor Detail

      • SPASSMlReasoner

        public SPASSMlReasoner​(java.lang.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​(java.lang.String binaryLocation)
        Constructs a new instance pointing to a specific SPASS
        Parameters:
        binaryLocation - of the SPASS executable on the hard drive
    • Method Detail

      • setCmdOptions

        public void setCmdOptions​(java.lang.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
      • queryProof

        public java.lang.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
      • evaluateResult

        private boolean evaluateResult​(java.lang.String output)
        Evaluates SPASS results.
        Parameters:
        output - of a SPASS query
        Returns:
        true if a proof was found, false otherwise