Re: [isabelle] Questions about arith





On Thu, 13 Apr 2006, Tom Ridge wrote:

Should I expect the following to be solved by arith? Or presburger? Or some other procedure? Or does the presence of the "f" go beyond what these procedures can handle? Is there an extension to presburger that can handle problems of this form?
Tom,
There are several reasons why arith fails to solve your goal.
1) Unfortunately presbugre works only over int (and nat). You use num?.
2) The abstraction over unknown terms works only if those are variables, and are not applied to bound variables. Both do not apply to your goal.

The f you use in the goal, is not "uninterpreted" since it has to satisfy the second conjuct. Here even qfree Preburger + uninterpreted functions would'nt help. I don'nt know of other decidable theories for this kind of goals.

Do you need arithmetic at all? the proof seems to only rely on ordering (may be sth is hidden in num).

Regards,
Amine.





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