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öße | Format | |
---|---|---|---|---|
2104.14445.pdf | 543,39 kB | Adobe PDF | Öffnen/Anzeigen |
Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons