Home

Welcome to the coq-library-undecidability wiki!

General information

• Guidelines on project design and structure

Detailed descriptions of mechanized undecidable problems

• Elementary Diophantine constraint solvability (H10C_SAT in Problems/H10C.v)
• Uniform Diophantine constraint solvability (H10UC_SAT in Problems/H10UC.v)
• Linear polynomial (over natural numbers) constraint solvability (LPolyNC_SAT in Problems/LPolyNC.v)
• Finite multiset constraint solvability (FMsetC_SAT in Problems/FMsetC.v)
• Recognizing axiomatizations of Hilbert-style calculi (HSC_AX in Problems/HSC.v)
• Provability in a fixed Hilbert-style calculus (HSC_PRV Γ in Problems/HSC.v)