The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Coq contributors and users,

My question is: What is the situation in Coq with a decidability in the
sense that if a formula is not derivable (provable) from a set of
hypotheses, Coq can conclude that formula is not decidable. To be clear, I
do not speak about the methods which can be modeled in Coq (like i.e.
Davis–Putnam procedure). I am interested in whether and for what areas
there exists automatisms in Coq which will tell you that something is
decidable / not decidable.

Thank you very much,

-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèilište u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Arts and Sciences
University of Rijeka, Croatia
-----------------------------