Class SPASSMlReasoner

    • 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
      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

        equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • 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