Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Coq-Club] Large bodies of knowledge


view this post on Zulip Email Gateway (Aug 19 2022 at 13:37):

From: Rene Vestergaard <vestergaard.rene@gmail.com>
Thanks for the references, Josef. I will read them with interest.

It may be worth stating, though, that the project I wrote about is more
type theory than expert system and that my questions probably pertain
mostly to mathematical-reasoning efforts.

Cheers,
Rene

view this post on Zulip Email Gateway (Aug 19 2022 at 13:42):

From: Rene Vestergaard <vestergaard.rene@gmail.com>
Dear Vladimir,

Thank you for sharing your considerations.

I must have misrepresented my position in the rush to ask my questions.

My intention was to cover what you state as being important under
'retrodiction', and it is the primary scientific justification I will
be putting forward for the project. More, the monograph in question fits
your description of the type of article you would want addressed, I believe.

My questions were about existing big formalizations, not so much what I
had done.

Cheers,
Rene

view this post on Zulip Email Gateway (Aug 19 2022 at 13:49):

From: Josef Urban <josef.urban@gmail.com>
This seems close to what has been tried in Project Halo. There was a
talk about automated reasoning challenges over the textbook "Campbell
Biology" last year at the CADE KInAR workshop:
http://www.michael-wessel.info/papers/kinar-2013-b.pdf . There is of
course also the recent $1B IBM is pumping into Watson:
http://www.reuters.com/article/2014/01/09/us-ibm-watson-idUSBREA0808U20140109

Josef


Last updated: Nov 21 2024 at 12:39 UTC