[isabelle] Linear Arithmetic
my project Columbo is slowly making progress. I currently wonder about
decidability of the halting problem for simple while programs, resp.
Rice's theorem. The following while program does clearly halt for all
integer values in i,s,ug,og and it's function can be expressed by a
What would Isabelle deduct from the code or it's denotation?
This archive was generated by a fusion of
Pipermail (Mailman edition) and