Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] an experimental tool for rewriting of real exp...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:49):

From: noam neer <noamneer@gmail.com>
hi everybody,

I did some work on an experimental tool for rewriting real expressions with
special functions (and some other proof assisting capabilities.) The tool
is standalone, but its proofs are meant to be translatable to Isabelle. The
tool's current name is the "Inequalitor."

The following doc gives very brief introduction to it, and a list of
problems that Isabelle 2017 can't solve in one command but the Inequalitor
can. I post it here just to see if there's an interest and hear some first
opinions. The tool itself and more documentation will be available soon.

Feel free to ask any questions and say anything about it.

thanx, Noam

<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#m_-4241733220311761072_m_641752627891317436_DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
ie_pa_overview.pdf


Last updated: Mar 28 2024 at 12:29 UTC