CPP'22 paper: "Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq"

Compilation:

tested with Coq versions 8.13.1 and 8.13.2 and Equations package 1.2.3+8.13
if you use opam, these can be installed with opam install coq.8.13.2 and opam install coq-equations.1.2.3+8.13
then run make in folder coq to compile project, should take less than 5 minutes

Name		Name	Last commit message	Last commit date
Latest commit History 12 Commits
website		website
.gitignore		.gitignore
Decidable.v		Decidable.v
Deduction.v		Deduction.v
Enumerable.v		Enumerable.v
FOL.v		FOL.v
FullSyntax.v		FullSyntax.v
Henkin.v		Henkin.v
Henkin2FOL.v		Henkin2FOL.v
Incompleteness.v		Incompleteness.v
ListLib.v		ListLib.v
Makefile		Makefile
PA.v		PA.v
SOL.v		SOL.v
Subst.v		Subst.v
Tarski.v		Tarski.v
Util.v		Util.v
VectorLib.v		VectorLib.v
_CoqProject		_CoqProject
readme.md		readme.md