Package com.articulate.sigma.tp

Class LEO

java.lang.Object
com.articulate.sigma.tp.LEO
public class LEO extends Object
Class for invoking the latest version of LEO-III from Java. It now uses THFnew to translate the knowledge base into THF syntax. To avoid bugs or crashes from the old THF implementation, only the connection to THFnew has been changed; all other logic remains the same. It should invoke a command like: ~/workspace/Leo-III/Leo-III-1.6/bin/leo3 /home/user/.sigmakee/KBs/SUMO.thf -t 60 -p

  • Field Details

    • qlist

      public StringBuilder qlist

    • output

      public List<String> output

    • axiomIndex

      public static int axiomIndex

    • debug

      public static boolean debug

  • Constructor Details

    • LEO

      public LEO()

  • 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 run() 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

    • assertFormula

      public static boolean assertFormula(String userAssertionTPTP, KB kb, List<Formula> parsedFormulas, boolean tptp)
      Add an assertion for inference.
      Parameters:
      userAssertionTPTP - asserted formula in the TPTP/TFF/THF syntax
      kb - Knowledge base
      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

    • writeStatements

      public void writeStatements(Set<String> stmts, String type)
      Write the statements to the temp-stmt.invalid input: '<'/> file

    • catFiles

      public void catFiles(String f1, String f2, String fout) throws IOException
      Read in two files and write their contents to a new file
      Throws:
      IOException

    • getUserAssertions

      public List<String> getUserAssertions(KB kb)

    • run

      public void run(KB kb, File kbFile, int timeout, Set<String> stmts) throws Exception
      Creates a running instance of LEO-III adding a set of statements in THF language to a file and then calling LEO. Note that any query must be given as a "conjecture"
      Parameters:
      stmts - should be the query but the list gets expanded here with any other prior user assertions
      Throws:
      Exception

    • main

      public static void main(String[] args) throws Exception
      Throws:
      Exception