Class SpassFolReasoner

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