Open augustepoiroux opened 8 months ago
This pull request adds the following files:
lisa-utils
ProofsConverter.scala
RunSolver.scala
lisa-examples
Kernel2Code.scala
TPTPSolver.scala
A few files in lisa-utils are modified to improve the string conversion correctness: Common.scala, FOLHelpers.scala, Sequents.scala
Common.scala
FOLHelpers.scala
Sequents.scala
TPTP parser script is also updated to handle edge cases: KernelParser.scala
KernelParser.scala
This pull request adds the following files:
lisa-utils:ProofsConverter.scala: methods to transform kernel proofs to Lisa code proofsRunSolver.scala: a class to run a solver for a given timelisa-examples:Kernel2Code.scala: showcases examples of kernel proofs conversion to Lisa code proofs.TPTPSolver.scala: extract, try to solve TPTP problems, and export LIsa code proofs of solved problems in a JSON file.A few files in
lisa-utilsare modified to improve the string conversion correctness:Common.scala,FOLHelpers.scala,Sequents.scalaTPTP parser script is also updated to handle edge cases:
KernelParser.scala