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.
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