Checkers v.2 redesign

Motivation

A flexible certifier

Currently Checkers expects certain proof formats and certify them. In GandALF, we presented a version of Checkers which can tackle two kinds of modal tableau proofs, with full proofs and with minimal information. This required creating two different FPCs for guiding the proof search in the LKF kernel. We would like to extend this approach to the full spectrum by using one FPC but allowing for holes to appear in the proof evidence. If the structure of the proof is not important but the relationship between quantifiers is, then one can omit the structure information.

Change of interpreter

Currently checkers is based on Teyjus and can certify proofs with little or no missing information. Currently, we are interested in showing the spectrum on which Checkers can allow the user to input different proof formats while still being able to certify them. I.e. the user can input only the "essential" information required for certifying the proof. This requires a more efficient implementation of lambda-prolog and we decided to give ELPI a try. There are many differences between the interpreters which will be tackled in this version.

Change from single kernel to multi-kernel approach

The current approach is based on having one trusted kernel (LKF) and on writing sophisticated FPCs for guiding the proof search in the kernel according to certain proof formats. This approach requires FPCs of increasing complexity and in order to allow for usability, we compose FPCs definitions so to abstract over irrelevant information. I.e. a resolution theorem prover implementer needs to know nothing about LKF since he can use an FPC from resolution to LKF and needs only write an FPC which can be composed with resolution. Our redesign will replace this approach by many kernels of different trust levels. In the above example, the resolution theorem prover impementer will certify his tool over a resolution kernel of lower trust level than LKF. Why should he use a less trusted kernel? Because this kernel will output a resolution proof which can always be send further in the chain to a more trusted kernel. Having LKF as the ultimate kernel. Of course, this approach blurs the line between a focused proof system and a non focused one since our kernels do not have to be focused any more. In addition, it requires adding clerks and experts to all kernels, which might not be so simple in practice. On the other hand, creating FPCs will be much simpler and we hope that it will greatly decrease the non-determinism involved in searching for proofs with missing information.

Steps

1. Target LKF and convert it to ELPI style
2. Modify lmf-singlefocus layer to a kernel + syntax + certificate interfaces + fpc from the output of the kernel to the LKF kernel
3. Test the above
4. Marco starts extending the above layer with other modal logics
   • Note, we can create all additional modal rules in the same kernel and control which one to use using experts!
   • Is there any interesting property we can gain of that, except cleaner code?
5. Tomer adds other kernels on top of that and rebuild the support for the last two versions of checkers

Step 1

Simple and required just changing the precedence of the operators &-&, etc. In order to use elpi, download the program, initialize the TJPATH containing all required files and run elpi on the main file (run with elpi -test when the goal is called main). Elpi doesnt require compilation and can work with both mod/sig files and elpi files. Use Elpi version of LFMTP 2016. Some later ones seem not to work properly with checkers.

Step 2

For this phase, we need to be able to create a kernel for LMF based on the AiML paper. First, I created the rules as written in the paper. It should be noted that the modal rule do not require higher-order quantification any more since we use labels externally and not as P(x) for label x. We still need implication so we cannot use prolog, for example, unless we use tricks which will add new clauses to the KB. The certificates interface was changed as well.

Step 3

In order to check it, I would like to be able to certify nested-sequents using this kernel. Once it does, I will add support for outputting the result, which will then be checked by the lkf kernel. One requirement here is to use exactly the same certificate for both lmf and lkf kernels. This will allow us to switch between the two but will keep the certificate a bit complex.