Package com.articulate.sigma.tp

Class EProver

java.lang.Object
com.articulate.sigma.tp.EProver
public class EProver extends Object

  • Field Details

  • Constructor Details

    • EProver

      public EProver(String executable, String kbFile) throws IOException
      Create a new batch specification file, and create a new running instance of EProver.
      Parameters:
      executable - A File object denoting the platform-specific EProver executable.
      kbFile - A File object denoting the initial knowledge base to be loaded by the EProver executable.
      Throws:
      IOException - should not normally be thrown unless either EProver executable or database file name are incorrect e_ltb_runner --interactive LTBSampleInput-AP.txt

    • EProver

      public EProver(String executable) throws IOException
      Create a running instance of EProver based on existing batch specification file with a max answer of 1.
      Parameters:
      executable - A File object denoting the platform-specific EProver executable.
      Throws:
      IOException

    • EProver

      public EProver(String executable, int maxAnswers) throws IOException
      Create a running instance of EProver based on existing batch specification file.
      Parameters:
      executable - A File object denoting the platform-specific EProver executable.
      maxAnswers - - Limit the answers up to maxAnswers only
      Throws:
      IOException

  • Method Details

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • getResult

      public ATPResult getResult()
      Get the full ATPResult for this run. This provides detailed execution metadata, SZS status, and error info.
      Returns:
      The ATPResult, or null if submitQuery hasn't been called

    • hasError

      public boolean hasError()
      Check if there was an error during execution.
      Returns:
      true if the result indicates an error

    • getSzsStatus

      public SZSStatus getSzsStatus()
      Get the SZS status from the last run.
      Returns:
      The SZSStatus, or SZSStatus.NOT_RUN if not run

    • addBatchConfig

      public static void addBatchConfig(String inputFilename, int timeout)
      Create or update batch specification file. e_ltb_runner processes a batch specification file; it contains a specification of the background theory, some options, and a number of individual job requests. It is used with the option --interactive. "inputFilename" is added into an existing batch specification file for inference.
      Parameters:
      inputFilename - contains TPTP assertions
      timeout - time limit in E

    • assertFormula

      public String assertFormula(String formula)
      Add an assertion for inference.
      Parameters:
      formula - asserted formula in the KIF syntax
      Returns:
      answer to the assertion

    • assertFormula

      public boolean assertFormula(String userAssertionTPTP, KB kb, EProver eprover, List<Formula> parsedFormulas, boolean tptp)
      Add an assertion for inference.
      Parameters:
      userAssertionTPTP - asserted formula in the TPTP syntax
      kb - Knowledge base
      eprover - an instance of EProver
      parsedFormulas - a lit of parsed formulas in KIF syntax
      tptp - convert formula to TPTP if tptp = true
      Returns:
      true if all assertions are added for inference TODO: This function might not be necessary if we find a way to directly add assertion into opened inference engine (e_ltb_runner)

    • terminate

      public void terminate() throws IOException
      Terminate this instance of EProver. After calling this function no further assertions or queries can be done.
      Throws:
      IOException - should not normally be thrown

    • submitQuery

      public String submitQuery(String formula, KB kb)
      Submit a query.
      Parameters:
      formula - query in the KIF syntax
      kb - current knowledge base
      Returns:
      answer to the query

    • runCustom

      public void runCustom(File kbFile, int timeout, Collection<String> commands) throws Exception
      Creates a running instance of Eprover with custom command line options.
      Parameters:
      kbFile - A File object denoting the initial knowledge base to be loaded by the Eprover executable.
      Throws:
      ExecutableNotFoundException - if the EProver executable is not found
      ProverCrashedException - if EProver crashes with a non-zero exit code
      ProverTimeoutException - if EProver times out
      Exception - for other errors

    • main

      public static void main(String[] args) throws Exception
      A simple test. Works as follows:
      1. start E;
      2. make an assertion;
      3. submit a query;
      4. terminate E
      Throws:
      Exception