Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-44489
Titel: Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
VerfasserIn: Kirst, Dominik
Larchey-Wendling, Dominique
Sprache: Englisch
Titel: Logical methods in computer science : LMCS
Bandnummer: 18
Heft: 2
Seiten: 17:1-17:29
Verlag/Plattform: Department of Theoretical Computer Science, Technical University of Braunschweig
Erscheinungsjahr: 2022
Freie Schlagwörter: Computer Science - Logic in Computer Science
Computer Science - Computation and Language
Mathematics - Logic
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Journalartikel / Zeitschriftenartikel
Abstract: 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 development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for monadic first-order logic, i.e. where the signature only contains at most unary function and relation symbols, as well as the enumerability of FSAT for arbitrary enumerable signatures. To showcase an application of Trakhtenbrot's theorem, we continue our reduction chain with a many-one reduction from FSAT to separation logic. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
DOI der Erstveröffentlichung: 10.46298/lmcs-18(2:17)2022
URL der Erstveröffentlichung: https://lmcs.episciences.org/9696
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-444894
hdl:20.500.11880/39719
http://dx.doi.org/10.22028/D291-44489
ISSN: 1860-5974
Datum des Eintrags: 25-Feb-2025
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Professur: MI - Prof. Dr. Gert Smolka
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
2104.14445.pdf543,39 kBAdobe PDFÖffnen/Anzeigen


Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons Creative Commons