LMF* Specification

[shaolintl]

LMF* is a sequent calculus for general modal logics. Below we specify the requirements: a) Proof evidence (is used for checking) b) Proof state (used by the checker to manage it state) c) Experts (fpc definitions)

For the systems: 1) LMFsf 2) LMF 3) LMF*

1) LMFsf - for single focus, was targeted by our previous version of checkers (see branch gandalf2016). LMFsf could target proofs from tableaux and other modal theorem provers. a) The proof evidence consisted of a triple A B C where: A) is the label of the formula we need to process. B) is an optional value given when the formula is a literal or a diamond to correlate them to complimentary literal or to the associated box. C) is the children of the formula (inductive definition of evidence) b) The proof state contains a list of computed indices (for storage) and an association between the indices of boxes and the corresponding concrete eigenvariables. c) Decide is deciding according to the index in the current node of the tree. Store uses the list in the state for choosing the right index for the formula. All (box) creates an association in the state and exists (dia) validates against this association using the optional argument in the certificate. All rules are setting the list in the state to contain one (unary) or two (binary) indices used for store. Literals are checked against their complementary in the context using again the optional argument in the certificate.

2) LMF allows multi focusing over LMFsf. a) We add to the triple also a unique multi focusing index (MFI). This index groups together formulas which we are focusing over. This value is optional. (b) and (c) do not change, i.e. we actually ignore this index in the LMF case.

• Maybe we might be able to come up with a general enough restriction on LMF based on MFI. @emmevolpe: yes, it would be nice.

3) LMF* applies restrictions to LMF in order to restrict the search space, based on additional info in the certificate. a) Each node will contain information on how to change the H value (see b) and on how to set the (optional) future of the formula. This future consists of one world currently (enough for K). b) The state contains H which is a set of the allowed current world of formulas which we can focus on
c) Based on LMF, in addition: Decide changes to ensure that the present of the formula to focus on is within H. It also uses the supplied future in the certificate in order to apply it as the future of the focused formula. Exists (dia) ensures that the future world is the future component in the label of the focused formula

• Note that we have a mechanism to allow deciding many times on the same formula occurrence in the theorem by using the bind component of an index. This component allows us to distinct deciding on formulas which are within the scope of different diamonds. @emmevolpe: I would say: at the moment we assume that we decide more than once only on diamond formulas (possibly because we want to relate them to different boxes). This means we can just use a mapping (index, label) in the proof state.

[shaolintl]

Marco, where do we use the multifocus index in the lmf-star fpc?

[emmevolpe]

As things are now, I would say that we use it only in the concrete instantiations, e.g., in OS. This is consistent with the paper, anyway.