Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] classical logic and decidability

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] classical logic and decidability


Chronological Thread 
  • From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] classical logic and decidability
  • Date: Wed, 26 Dec 2012 07:45:42 +0100

Hi,

Thanks for your explanations about decidability. Very interesting,
made me think a lot, I think a true definition of decidability in
Coq should be very complicated, since it implies that we define the
notion of algorithm, and tutti quanti. I think Bruno Barras' thesis
(Coq in Coq) contains this.

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/



Archive powered by MHonArc 2.6.18.

Top of Page