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: Nov 21 2024 at 12:39 UTC