Stream: Coq users

Topic: What happened to CAD?

view this post on Zulip Luigi Massacci (Feb 01 2024 at 14:59):

Hello! I was really excited to see that Cylindrical Algebraic Decomposition has been formalised in Coq, with an attached procedure for it, but I have two possibly ignorant questions:
a) Is there some documentation in the style of say ring, that explains how to use it in practice (alternatively, maybe one of the papers about it were it is explained? The ones I’ve seen seem all to focus on the formalisation aspects)
b) How did it work in practice? I can’t seem to find instances in mathcomp / other Coq repos. Was it too slow?

view this post on Zulip Karl Palmskog (Feb 01 2024 at 16:51):

Is this about this repo?

Last updated: Jun 23 2024 at 04:03 UTC