Roadmap for Checkers - proofcert/checkers GitHub Wiki

Marco and Tomer met on 19/1/2017

Problems with current implementation

Framework is not really a framework as different proof formats do not really need the different layers

Add ability to use holes in proof objects. This ability already exists but fails when too many holes (find out why?!)
Add ability to give just essential information like relationship between diamonds and boxes

Understand why more abstraction leads to failure while less abstraction does not terminate (abstraction means replacing terms by variables). Would switching to ELPI help?
Separate essential info from proof structure so we can abstract separately on each
The two will give us the whole spectrum for proof evidence which will support
giving full to none essential info
giving full to none tree structure info together they allow checkers also to serve as a fully automated as well as "interactive" theorem prover as the initial certificate with holes will contain all info of the users (similar to tactics?)

First do the separation since it will allow us more flexibility on understanding why adding holes fails
Then do the understanding + required refactoring (maybe not crucial for first version?)
Try it out on FV tableaux, fully automated OS as well as interactive things

Fest journal (February?)
JAR Special Issue on Automated Reasoning Systems (April 3rd)
Conferences: Cade (February 18th) , CSL (March 31st), Tableaux (April 25th), ITP (April 10th)

Use separation in order to be able to certify multiple tableau modal provers and submit to Tableau
Use the fact we have the full spectrum of information to build a prover which can target everything from full automation to full information - submission to ITP, Cade, CSL, journal?