Dominik Kirst

Publication Activity (10 Years)

Years Active: 2016-2024
Publications (10 Years): 30

Top Topics

Quantifier Free

Finite Model Theory

Epistemic Logic

Top Venues

J. Autom. Reason.

Publications

Marc Hermes, Dominik Kirst
An Analysis of Tennenbaum's Theorem in Constructive Type Theory. Log. Methods Comput. Sci. 20 (1) (2024)
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
Separating Markov's Principles. LICS (2024)
Yannick Forster, Dominik Kirst, Niklas Mück
The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. CSL (2024)
Ian Shillito, Dominik Kirst
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. CPP (2024)
Dominik Kirst, Marc Hermes
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. J. Autom. Reason. 67 (1) (2023)
Dominik Kirst, Benjamin Peters
Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability. CSL (2023)
Marc Hermes, Dominik Kirst
An Analysis of Tennenbaum's Theorem in Constructive Type Theory. CoRR (2023)
Yannick Forster, Dominik Kirst, Niklas Mück
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. CoRR (2023)
Yannick Forster, Dominik Kirst, Niklas Mück
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. APLAS (2023)
Dominik Kirst
Computational Back-And-Forth Arguments in Constructive Type Theory. ITP (2022)
Dominik Wehr, Dominik Kirst
Material Dialogues for First-Order Logic in Constructive Type Theory. WoLLIC (2022)
Christian Hagemeier, Dominik Kirst
Constructive and mechanised meta-theory of IEL and similar modal logics. J. Log. Comput. 32 (8) (2022)
Dominik Kirst, Dominique Larchey-Wendling
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. Log. Methods Comput. Sci. 18 (2) (2022)
Johannes Hostert, Andrej Dudenhefner, Dominik Kirst
Undecidability of Dyadic First-Order Logic in Coq. ITP (2022)
Mark Koch, Dominik Kirst
Undecidability, incompleteness, and completeness of second-order logic in Coq. CPP (2022)
Marc Hermes, Dominik Kirst
An Analysis of Tennenbaum's Theorem in Constructive Type Theory. FSCD (2022)
Christian Hagemeier, Dominik Kirst
Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic. LFCS (2022)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput. 31 (1) (2021)
Dominik Kirst, Dominique Larchey-Wendling
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. CoRR (2021)
Dominik Kirst, Felix Rech
The generalised continuum hypothesis implies the axiom of choice in Coq. CPP (2021)
Dominik Kirst, Marc Hermes
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. ITP (2021)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version). CoRR (2020)
Dominik Kirst, Dominique Larchey-Wendling
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. IJCAR (2) (2020)
Dominik Kirst, Dominique Larchey-Wendling
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory. CoRR (2020)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. LFCS (2020)
Dominik Kirst, Gert Smolka
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. J. Autom. Reason. 63 (2) (2019)
Yannick Forster, Dominik Kirst, Gert Smolka
On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP (2019)
Dominik Kirst, Gert Smolka
Large model constructions for second-order ZF in dependent type theory. CPP (2018)
Dominik Kirst, Gert Smolka
Categoricity Results for Second-Order ZF in Dependent Type Theory. ITP (2017)
Dominik Kirst, Andreas Bulling
On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input. CHI Extended Abstracts (2016)