Home

Jump to bottom Edit New page

Andrej Dudenhefner edited this page Nov 25, 2019 · 9 revisions

Welcome to the coq-library-undecidability wiki!

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)