Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens

We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our developmen...

Deskribapen osoa

Xehetasun bibliografikoak

Egile Nagusiak:	Dominik Kirst, Dominique Larchey-Wendling
Formatua:	Artigo
Hizkuntza:	Inglês
Argitaratua:	Logical Methods in Computer Science e.V. 2022-06-01
Saila:	Logical Methods in Computer Science
Gaiak:	computer science - logic in computer science computer science - computation and language mathematics - logic
Sarrera elektronikoa:	https://lmcs.episciences.org/7422/pdf
Etiketak:	Etiketa erantsi Etiketarik gabe, Izan zaitez lehena erregistro honi etiketa jartzen!