| Publication | Date of Publication | Type |
|---|
| Conditional normative reasoning as a fragment of HOL | 2024-12-09 | Paper |
| Who finds the short proof? | 2024-11-15 | Paper |
| Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments | 2024-10-14 | Paper |
| Mathematical proof between generations | 2024-09-26 | Paper |
| Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics" | 2024-03-10 | Dataset |
| Category theory in Isabelle/HOL as a basis for meta-logical investigation | 2024-02-28 | Paper |
| Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy | 2024-02-08 | Paper |
| Solving modal logic problems by translation to higher-order logic | 2024-01-16 | Paper |
| On Gödel and the Nonexistence of Time – Gödel und die Nichtexistenz der Zeit | 2023-10-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6157248 | 2023-06-20 | Paper |
| Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint | 2023-05-24 | Paper |
| Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding | 2023-03-29 | Paper |
| Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract) | 2022-11-04 | Paper |
| Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic | 2022-11-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5869628 | 2022-09-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5869627 | 2022-09-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5869572 | 2022-09-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5102453 | 2022-09-07 | Paper |
| Computer-Supported Analysis of Arguments in Climate Engineering | 2022-08-30 | Paper |
| Computer-Supported Exploration of a Categorical Axiomatization of Modeloids | 2022-08-30 | Paper |
| Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers | 2022-08-14 | Paper |
| A Simplified Variant of G\"odel's Ontological Argument | 2022-02-13 | Paper |
| Public announcement logic in HOL | 2021-12-01 | Paper |
| Extensional higher-order paramodulation in Leo-III | 2021-11-23 | Paper |
| Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support | 2020-11-16 | Paper |
| Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument | 2020-10-15 | Paper |
| Public Announcement Logic in HOL | 2020-10-02 | Paper |
| Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments | 2020-08-10 | Paper |
| Mechanised assessment of complex natural-language arguments using expressive logic combinations | 2020-05-13 | Paper |
| On Reductions of Hintikka Sets for Higher-Order Logic | 2020-04-16 | Paper |
| MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY | 2020-03-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219925 | 2020-03-09 | Paper |
| Automating free logic in HOL, with an experimental application in category theory | 2020-03-03 | Paper |
| Computer-supported Exploration of a Categorical Axiomatization of Modeloids | 2019-10-27 | Paper |
| Ωmega: Towards a mathematical assistant | 2019-10-01 | Paper |
| Extensional Higher-Order Paramodulation in Leo-III | 2019-07-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5224901 | 2019-07-24 | Paper |
| Computer Science and Metaphysics: A Cross-Fertilization | 2019-05-01 | Paper |
| What is a proof? What should it be? | 2019-04-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4619819 | 2019-02-07 | Paper |
| Theorem Provers For Every Normal Modal Logic | 2019-01-10 | Paper |
| The higher-order prover Leo-III | 2018-10-18 | Paper |
| A deontic logic reasoning infrastructure | 2018-09-06 | Paper |
| Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL | 2018-02-23 | Paper |
| The Higher-Order Prover Leo-III (Extended Version) | 2018-02-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5357221 | 2017-09-14 | Paper |
| Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic | 2017-08-11 | Paper |
| Cut-elimination for quantified conditional logic | 2017-07-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5282959 | 2017-07-18 | Paper |
| Computer-assisted analysis of the Anderson-Hájek ontological controversy | 2017-04-20 | Paper |
| Higher-Order Modal Logics: Automation and Applications | 2017-03-30 | Paper |
| Proofs and Reconstructions | 2017-02-27 | Paper |
| Agent-Based HOL Reasoning | 2016-09-28 | Paper |
| Automating Free Logic in Isabelle/HOL | 2016-09-28 | Paper |
| Axiomatizing Category Theory in Free Logic | 2016-09-06 | Paper |
| Effective Normalization Techniques for HOL | 2016-09-05 | Paper |
| The higher-order prover \textsc{Leo}-II | 2016-05-26 | Paper |
| On Logic Embeddings and Gödel’s God | 2016-02-25 | Paper |
| There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners | 2016-01-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3457212 | 2015-12-11 | Paper |
| Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics | 2015-12-11 | Paper |
| LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners | 2015-11-20 | Paper |
| Interacting with Modal Logics in the Coq Proof Assistant | 2015-10-20 | Paper |
| HOL Based First-Order Modal Logic Provers | 2014-01-17 | Paper |
| \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems | 2013-12-20 | Paper |
| Assertion-level proof representation with under-specification | 2013-09-09 | Paper |
| Formalization, Mechanization and Automation of G\"odel's Proof of God's Existence | 2013-08-21 | Paper |
| Quantified multimodal logics in simple type theory | 2013-04-08 | Paper |
| Embedding and automating conditional logics in classical higher-order logic | 2013-02-18 | Paper |
| Combining and automating classical and non-classical logics in classical higher-order logics | 2012-01-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086775 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086787 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3075241 | 2011-02-10 | Paper |
| Multimodal and intuitionistic logics in simple type theory | 2010-12-14 | Paper |
| Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) | 2010-11-22 | Paper |
| Combining Logics in Simple Type Theory | 2010-08-24 | Paper |
| Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega | 2009-09-18 | Paper |
| Progress in the Development of Automated Theorem Proving for Higher-Order Logic | 2009-07-28 | Paper |
| Cut-Simulation and Impredicativity | 2009-04-29 | Paper |
| Cut-Simulation in Impredicative Logics | 2009-03-12 | Paper |
| LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) | 2008-11-27 | Paper |
| THF0 – The Core of the TPTP Language for Higher-Order Logic | 2008-11-27 | Paper |
| Combined reasoning by automated cooperation | 2008-09-23 | Paper |
| KI 2004: Advances in Artificial Intelligence | 2008-03-14 | Paper |
| Computer supported mathematics with \(\Omega\)MEGA | 2007-02-20 | Paper |
| Towards computer aided mathematics | 2007-02-20 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Theorem Proving in Higher Order Logics | 2006-07-06 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Higher-order semantics and extensionality | 2005-08-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4664927 | 2005-04-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4809051 | 2004-08-12 | Paper |
| Automatic Learning of Proof Methods in Proof Planning | 2004-05-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4428312 | 2003-09-15 | Paper |
| Comparing approaches to resolution based higher-order theorem proving | 2003-04-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4797443 | 2003-03-13 | Paper |
| Towards learning new methods in proof planning | 2002-06-13 | Paper |
| Distributed assertion retrieval | 2002-02-14 | Paper |
| \(\Omega\)-ANTS -- An open approach at combining interactive and automated theorem proving | 2001-10-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499162 | 2001-03-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263170 | 2000-05-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4249891 | 2000-01-12 | Paper |
