# [isabelle] 2 questions

 Dear Isabelle users, I am trying to develop a tactic for a sequente calculus for labelled modal logics (from Luca Viganò "Labelled non-Classical Logics", Kluwer, 2000) and I am facing 2 problems that might have been already solved in other context by some of you: a) In some of those logics an upper bound on the number of applications of non-safe rules (i.e. BoxLeft) can be found depending on the complexity of the formula to be established (or not establised). To represente this an ML-function has to be written that calculates the complexity of the formula (easy). However it is not clear to me how I can write a tactic looking like REPEAT_DETERM_N (complexity ??formula??) b) (Saturation) The BoxLeft rule looks like ([|x:[]A; xRy|]==>R)==>([|x:[]A; xRy; y:A|]==>R) and is somehow similar to the left rule for the universal quantifier. There may be several unification possibilities, for example if xRy and xRy1 are present in the premises. I would like to have a rule that uses all possible unifications. For that particular case the rule ([|x:[]A; xRy; xRy1|]==>R)==>([|x:[]A; xRy; xRy1; y:A;y1:A|]==>R) would do. This is similar to having a left rule for the universal quantifier that would instanciate the predicate in all unifiable terms available. Many thanks, fmd ps: just direct me to some code if you have already solved somethig similar ```-- Francisco Miguel Dionísio Departamento de Matemática Instituto Superior Técnico tel: 218417143 fmd at math.ist.utl.pt```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.