| Title: |
A Coq Library for Mechanised First-Order Logic |
| Authors: |
Kirst, Dominik; Hostert, Johannes; Dudenhefner, Andrej; Forster, Yannick; Hermes, Marc; Koch, Mark; Larchey-Wendling, Dominique; Mück, Niklas; Peters, Benjamin; Smolka, Gert; Wehr, Dominik |
| Contributors: |
Programming Systems Lab Saarland; Saarland University Saarbrücken; Logic, Proof Theory and Programming (TYPES); Department of Formal Methods (LORIA - FM); Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
| Source: |
The Coq Workshop 2022 ; https://hal.science/hal-03756335 ; The Coq Workshop 2022, Aug 2022, Haifa, Israel |
| Publisher Information: |
HAL CCSD |
| Publication Year: |
2022 |
| Collection: |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
| Subject Terms: |
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]; [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM]; [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]; [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]; [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]; [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] |
| Subject Geographic: |
Haifa; Israel |
| Description: |
International audience ; We report about an ongoing collaborative effort to consolidate several Coq developments concerning metamathematical results in first-order logic [1, 2, 11, 10, 8, 7, 6, 15, 12] into a single library. We first describe the framework regarding the representation of syntax, deduction systems, and semantics as well as its instantiation to axiom systems and tools for user-friendly interaction. Next, we summarise the included results mostly connected to completeness, undecidability, and incompleteness. Finally, we conclude by reporting on challenges experienced and anticipated during the integration. The current status of the project can be tracked in a public fork of the Coq Library of Undecidability Proofs [3]. Framework In principle, we follow ideas and suggestions present in various approaches [14, 9, 5, 4, 13] to the representation of first-order logic in CIC. Over the span of our initial projects we tried out several variants and found the final framework to be most suitable. Notably, a previous version used the Autosubst 2 tool [16] to generate the syntax, which we decided to avoid in later versions due to its use of function extensionality. The final framework, however, still follows the same design principles for binding and substitution. The syntax is represented by inductive types for terms t : T and formulas ϕ : F depending on signatures of function symbols f and relation symbols P as well as a collection of binary connectives 2 and quantifiers ∇ |
| Document Type: |
conference object |
| Language: |
English |
| Relation: |
hal-03756335; https://hal.science/hal-03756335; https://hal.science/hal-03756335/document; https://hal.science/hal-03756335/file/Coq2022-01-01-first-order-logic.pdf |
| Availability: |
https://hal.science/hal-03756335; https://hal.science/hal-03756335/document; https://hal.science/hal-03756335/file/Coq2022-01-01-first-order-logic.pdf |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.C9DBED62 |
| Database: |
BASE |