Re: [isabelle] Partial Linear Arithmetic



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





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