The Coq mailing list

[Yannick Forster <forster AT ps.uni-saarland.de>]

Hi Francisco,

we have a paper on undecidability results related to first-order logic 
at the upcoming CPP conference, coming with a formalisation of FOL in Coq:

Yannick Forster, Dominik Kirst, Gert Smolka: On Synthetic Undecidability 
in Coq, with an Application to the Entscheidungsproblem 
(https://www.ps.uni-saarland.de/extras/fol-undec/)

Besides the work of Russell O'Connor that Cody mentioned there are also 
substantial formalisations by Hugo Herbelin and Gyesik Lee, for instance 
covered in

Hugo Herbelin, SunYoung Kim, Gyesik Lee:  Formalizing
the meta-theory of first-order predicate logic 
(https://doi.org/10.4134/JKMS.j160546, https://github.com/liganega/trace)

Hope that helps!

Yannick

--
PhD student, Programming Systems Lab, Saarland University
https://www.ps.uni-saarland.de/~forster/


On 17/12/2018 16:39, Francisco Trucco wrote:
> Hi all,
>
> I was wondering if any of you knew of a*first order logic or second 
> order logic formalization in Coq*. In particular, I am looking for 
> something similar to Coq in Coq 
> <https://github.com/coq-contribs/coq-in-coq> but with FOL or SOL.
>
> Thanks a lot!
>
> Francisco Trucco