The Coq mailing list

[Alex Shkotin <alex.shkotin AT gmail.com>]

and have a look here https://ontologforum.org/index.php/OntologySummit

пн, 25 окт. 2021 г. в 18:24, Agnishom Chattopadhyay <agnishom AT cmi.ac.in>:

This is interesting. I vaguely know some things about ontology but nothing about the modern developments in this subject.

What are the OWL and DL frameworks referenced in this thread? Also, do you have any approachable reading recommendations about the contemporary developments in ontology? I am especially interested in the kind of frameworks that involve rigorous formalisms.

On Sun, Oct 24, 2021 at 2:49 AM Alex Shkotin <alex.shkotin AT gmail.com> wrote:

Thanks, Abhishek and All!

The origin of my question is here https://groups.google.com/g/ontolog-forum/c/q9XT9WCxM_c

Alex

вс, 24 окт. 2021 г. в 08:02, Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

for any 2 closed, computable real numbers r1 r2, r1>r2 can be proved automatically if it is true: just compute enough "digits" of r1 and r2, as Agnishom suggests. \pi and e are computable and are already defined in the CORN library in a computable ("constructive") way that lets you COMPUTE arbitrarily tight Q approximations to them.

https://github.com/coq-community/corn/blob/master/reals/fast/CRpi.v

https://github.com/coq-community/corn/blob/master/reals/fast/CRexp.v

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Oct 22, 2021 at 11:44 AM Alex Shkotin <alex.shkotin AT gmail.com> wrote:

Hi All!

How in Coq define π and e and prove that π>e?

Alex