Class SpassFolReasoner

    • 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
      SpassFolReasoner​(java.lang.String binaryLocation)
      Constructs a new instance pointing to a specific SPASS
      SpassFolReasoner​(java.lang.String binaryLocation, Shell bash)
      Constructs a new instance pointing to a specific SPASS Prover.
    • Method Summary

      Modifier and Type Method Description
      boolean equivalent​(FolBeliefSet kb, FolFormula a, FolFormula b)
      This method determines whether two formulas are equivalent wrt.
      private boolean evaluateResult​(java.lang.String output)
      Evaluates SPASS results.
      java.lang.Boolean query​(FolBeliefSet kb, FolFormula query)
      Queries the given belief base for the given formula.
      java.lang.String queryProof​(FolBeliefSet 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

      • SpassFolReasoner

        public SpassFolReasoner​(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
      • SpassFolReasoner

        public SpassFolReasoner​(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​(FolBeliefSet kb,
                                           Formula query)
        Determines the answer wrt. to the given query and returns the proof (if applicable). May decrease SPASS's performance, use query(FolBeliefSet,FolFormula) if only a yes/no result is needed.
        Parameters:
        kb - the knowledge base
        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
      • equivalent

        public boolean equivalent​(FolBeliefSet kb,
                                  FolFormula a,
                                  FolFormula b)
        Description copied from class: FolReasoner
        This method determines whether two formulas are equivalent wrt. to the given knowledge base.
        Specified by:
        equivalent in class FolReasoner
        Parameters:
        kb - the knowledge base
        a - the first formula.
        b - the second formula.
        Returns:
        the answer to the query.