6 citations · 7 across the 4 of their papers we have counts for
4 papers
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Tim S. Lyon, Agata Ciabattoni, Didier Galmiche +5
This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuiti…
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
Dominik Kirst, Dominique Larchey-Wendling
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 fu…
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
Dominik Kirst, Dominique Larchey-Wendling
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 fu…
Hilbert's Tenth Problem in Coq (Extended Version)
Dominique Larchey-Wendling, Yannick Forster
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the fi…