Running solvers on TPTP + converting kernel proofs to Lisa code#208

Open

augustepoiroux wants to merge 24 commits intoepfl-lara:mainfrom

augustepoiroux:kernel2tactic

Commits on Feb 12, 2024

Add first draft for kernel2tactic transformation
augustepoiroux
committed
Add proofsteps reference
augustepoiroux
committed
Fix some kernel2code issues when refering to previous steps
augustepoiroux
committed
First stable conversion from kernel to code proofs
augustepoiroux
committed
Refactor code + thenHave
augustepoiroux
committed
Handle more cases
augustepoiroux
committed
Add todo list
augustepoiroux
committed
Update and clean scproof2code method
augustepoiroux
committed
Refactor files
augustepoiroux
committed
Update + fix TPTP problem parser
augustepoiroux
committed
Add TPTPSolver class for solving problems from TPTP library using Tableau tactic
augustepoiroux
committed
Update TPTP problem solver code
augustepoiroux
committed
Separate the solver runner logic from the TPTP data extraction
augustepoiroux
committed
Fix and improve kernel2code and asFront methods
augustepoiroux
committed
Fix Sequent toString method
augustepoiroux
committed
Add proof checks in TPTPSolver
augustepoiroux
committed
Improve conversion from kernel to code
augustepoiroux
committed
Add standalone file generator for theorems and proofs + cleanup
augustepoiroux
committed
Add documentation to the lisa proof code generator
augustepoiroux
committed
Fix TPTP parsing of atomic formula
augustepoiroux
committed
Improve the Lisa code generator from SCProof
augustepoiroux
committed
Export proofs extracted from TPTP to JSON
augustepoiroux
committed
Fix equality infix printing + parsing issues
augustepoiroux
committed
Remove user-specific paths
augustepoiroux
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Running solvers on TPTP + converting kernel proofs to Lisa code#208

Running solvers on TPTP + converting kernel proofs to Lisa code#208
augustepoiroux wants to merge 24 commits intoepfl-lara:mainfrom
augustepoiroux:kernel2tactic

Commits on Feb 12, 2024

Add first draft for kernel2tactic transformation

Add proofsteps reference

Fix some kernel2code issues when refering to previous steps

First stable conversion from kernel to code proofs

Refactor code + thenHave

Handle more cases

Add todo list

Update and clean scproof2code method

Refactor files

Update + fix TPTP problem parser

Add TPTPSolver class for solving problems from TPTP library using Tableau tactic

Update TPTP problem solver code

Separate the solver runner logic from the TPTP data extraction

Fix and improve kernel2code and asFront methods

Fix Sequent toString method

Add proof checks in TPTPSolver

Improve conversion from kernel to code

Add standalone file generator for theorems and proofs + cleanup

Add documentation to the lisa proof code generator

Fix TPTP parsing of atomic formula

Improve the Lisa code generator from SCProof

Export proofs extracted from TPTP to JSON

Fix equality infix printing + parsing issues

Remove user-specific paths

Running solvers on TPTP + converting kernel proofs to Lisa code#208augustepoiroux wants to merge 24 commits intoepfl-lara:mainepfl-lara/lisa:mainfrom augustepoiroux:kernel2tacticaugustepoiroux/lisa:kernel2tacticCopy head branch name to clipboard

Commits

Commits on Feb 12, 2024

Running solvers on TPTP + converting kernel proofs to Lisa code#208
augustepoiroux wants to merge 24 commits intoepfl-lara:mainfrom
augustepoiroux:kernel2tactic