*To*: Jens Doll <jd at cococo.de>*Subject*: Re: [isabelle] Partial Linear Arithmetic*From*: Amine Chaieb <ac638 at cam.ac.uk>*Date*: Fri, 30 Jan 2009 19:28:55 +0000*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <OFBC51876D.967173AC-ONC125754E.0028B786-C125754E.0029FC2E@cococo.de>*References*: <OFBC51876D.967173AC-ONC125754E.0028B786-C125754E.0029FC2E@cococo.de>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 2.0.0.19 (X11/20090105)

Dear Jens, I find it somehow difficult to isolate the problem (the formula) to be proved. Could you send the formula? Is it over the integers or over the reals? If it is the latter, then there is a procedure that would eliminate you the linear quantifiers. It is described in [2] Amine Chaieb. Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL. In Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, and Freek Wiedijk, editors, /AISC/MKM/Calculemus/, volume 5144 of /Lecture Notes in Computer Science/, pages 246-260. Springer-Verlag, July 2008. If it is over the integers though, then I only know of a procedure by Weispfenning 1990, which has been reconsidered recently (2006 I think) by Sturm. It might be implemented in REDLOG/REDUCE. That theory does not admit quantifier elimination in the usual sense. You need to introduce a new kind of quantifiers (not eliminated). I also think it is not decidable. Hope it helps, Amine. Jens Doll wrote: > Isabelle now runs on my machine again and I thank Florian for helping me > with the installation. So I was able to enter some simple lemmata and to > rework my verification samples. (Excuse me for the buggy version > beforehand.) I added a third sample > > http://cococo.de/products/windows/Columbo/sample3.html > > which now contains a more difficult example: the function is rational and > multivariate, but the loop is linear in one variable. > > Jens > > P.S.: I still did not find the correct formula for the modular case, > sample2.html. Isabelle declines to solve the lemma. Does anyone know, > what's wrong there? > >

**Follow-Ups**:**Re: [isabelle] Partial Linear Arithmetic***From:*Jens Doll

**References**:**[isabelle] Partial Linear Arithmetic***From:*Jens Doll

- Previous by Date: Re: [isabelle] Partial Linear Arithmetic
- Next by Date: [isabelle] Having trouble on Producing an inductive lemma for the following inductive definition.
- Previous by Thread: Re: [isabelle] Partial Linear Arithmetic
- Next by Thread: Re: [isabelle] Partial Linear Arithmetic
- Cl-isabelle-users January 2009 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