Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Hermes, Marc"'
Autor:
Hermes, Marc, Kirst, Dominik
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 1 (March 7, 2024) lmcs:11042
Tennenbaum's theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit, analyze and
Externí odkaz:
http://arxiv.org/abs/2302.14699
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Studies in Health Technology & Informatics; 2024, Vol. 316, p731-735, 5p
Publikováno v:
Studies in Health Technology & Informatics; 2024, Vol. 316, p741-745, 5p
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Kirst, Dominik, Hostert, Johannes, Dudenhefner, Andrej, Forster, Yannick, Hermes, Marc, Koch, Mark, Larchey-Wendling, Dominique, Mück, Niklas, Peters, Benjamin, Smolka, Gert, Wehr, Dominik
Publikováno v:
The Coq Workshop 2022
The Coq Workshop 2022, Aug 2022, Haifa, Israel
The Coq Workshop 2022, Aug 2022, Haifa, Israel
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 fram
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::e0cef6ebb1ad74f6045370581b93c0e8
https://hal.science/hal-03756335/file/Coq2022-01-01-first-order-logic.pdf
https://hal.science/hal-03756335/file/Coq2022-01-01-first-order-logic.pdf
Autor:
Hermes, Marc, Kirst, Dominik
Tennenbaum’s theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit and genera
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::786737b0c0d47cd377d0f892fc4c97b2
Autor:
Kirst, Dominik, Hermes, Marc
We mechanise the undecidability of various first-order axiom systems in Coq, employing the synthetic approach to computability underlying the growing Coq Library of Undecidability Proofs. Concretely, we cover both semantic and deductive entailment in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d5f2c9f1669dd3750a67753ffbc262d3