Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Wehr, Dominik"'
Autor:
Leigh, Graham E., Wehr, Dominik
We consider cyclic proof systems in which derivations are graphs rather than trees. Such systems typically come with a condition that isolates which derivations are admitted as 'proofs', known as a the soundness condition. This soundness condition fr
Externí odkaz:
http://arxiv.org/abs/2301.07544
Autor:
Leigh, Graham E., Wehr, Dominik
Publikováno v:
In Annals of Pure and Applied Logic December 2024 175(10)
Publikováno v:
Journal of Logic and Computation, Volume 31, Issue 1, January 2021, Pages 112-151
We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduct
Externí odkaz:
http://arxiv.org/abs/2006.04399
Autor:
Afshari, Bahareh, Wehr, Dominik
Publikováno v:
In Information and Computation November 2022
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.
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.
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:
Forster, Yannick, Larchey-Wendling, Dominique, Dudenhefner, Andrej, Heiter, Edith, Kirst, Dominik, Kunze, Fabian, Smolka, Gert, Spies, Simon, Wehr, Dominik, Wuttke, Maximilian
Publikováno v:
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1017/S0960129597002302⟩
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1017/S0960129597002302⟩
International audience; We propose a talk on our library of mechanised reductions to establish undecidability results in Coq. The library is a collaborative effort, growing constantly and we are seeking more outside contributors willing to work on un
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::5ef40888eb477ac9377613af6b2d75b0
https://hal.archives-ouvertes.fr/hal-02944217
https://hal.archives-ouvertes.fr/hal-02944217
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.