Cleaning the implementation

[shaolintl]

The problem:

Currently, we encode from modal into FOL the formula of the certificate and then we use several layers of FPCs in order to translate between the layers.

Marco would like to have concrete kernels for each layer and have a clean translation between evidence in one into the next kernel.

So we use the FPC to generate an output evidence which will be fed to the next FPC in the chain.

This will impose having different kernels for each layer. I.e. on the LMFos layer, there is no decide rule!

[shaolintl]

@emmevolpe, I am looking at creating the kernel according to the paper and see there are some differences between the proof format we expect right now using the singlefoc FPC and the calculus defined in the paper.

• we deal with the two indices (node and the optional pair), where is this information in the calculus. I am asking since although the first index seems clear, what is the relation of the second index to the calculus? Can it easily be obtained?

[emmevolpe]

The second index is either (i) the index of the box related to a diamond or (ii) the index of a complementary literal. I think in both cases these indexes should be used by the expert predicates (of the diamond and init rule, respectively).

Notice also that we do not use labels explicitly in our proof format, because we infer it from the eigenvariables used, but the language of LMF and LMF_* in the papers is a labeled language.

[shaolintl]

@emmevolpe It seems that the clerks and experts give us several advantages when writing the kernel.

1. we can put all modal rules within the same kernel and the diamond expert will choose the right rule (having a flag in the certificate). We can also adapt the box clerk (although he won't be just a clerk anymore).
2. can we use the same for the different lkf versions? I.e. one calculus which supports all? You claimed that you dont see the point in having three layers. Is it still the case when having different modal logics? Can we use just one layer?

[emmevolpe]

1. What do you mean by all modal rules?
2. What I meant was that I don't see the point in having more layers if they don't "use" each other in any way and we use only the external one. I am not sure I understand what you mean here by just one calculus: would it be LMF_*?

[shaolintl]

1. I mean that the certificate will tell if we apply K diamond or S4 diamond but both will be part of the same kernel
2. Yes, LMF_* if it makes no difference for other modal logics than K

[shaolintl]

Another question, How do you come up with the label in the cut rule in LMF? I guess it should be supplied by the expert, right?

[emmevolpe]

About the cut, yes.

I am not sure I am getting the other points. To me, in LMF*, there should be only one diamond rule; the decide should have several versions instead (in principle, in the distinct LMF_OS, LMF_NS etc. unless we want to put everything together), but depending on the formalism and not on the logic.
Treating other logics means adding (relational) rules to the calculus.

Let's try to meet soon :)

[shaolintl]

:) good idea. I am looking on p. 10 in AiML and it seems that you have different versions for diamonds and boxes but right, I found the right page (p. 8) which raises even an harder question!

It seems that a whole treatment should be possible on relations using the certificates, the certificate should tell which relations to pick and what operation to apply on them. Am I right? So we need some neutral rule that just works on relations and is backed up by an expert.
It seems even more probable that you would like to have a new expert for each modal rule, right? Some of them just pick the relation we want to process but others have to supply new worlds, like T and D. What do you think?