*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] 2 questions*From*: "F. Miguel Dionisio" <fmd at math.ist.utl.pt>*Date*: Fri, 31 Mar 2006 11:26:50 +0100*Cc*: marco <marco at uma.pt>*Organization*: IST (Dep. de Matemática)*User-agent*: Thunderbird 1.5 (Windows/20051201)

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 |

- Previous by Date: [isabelle] Theory of finite maps
- Next by Date: Re: [isabelle] thm_deps
- Previous by Thread: [isabelle] Theory of finite maps
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list