Publication | Date of Publication | Type |
---|
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 |
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/Q5869572 | 2022-09-28 | Paper |
https://portal.mardi4nfdi.de/entity/Q5869627 | 2022-09-28 | Paper |
https://portal.mardi4nfdi.de/entity/Q5869628 | 2022-09-28 | Paper |
https://portal.mardi4nfdi.de/entity/Q5102453 | 2022-09-07 | Paper |
Computer-Supported Exploration of a Categorical Axiomatization of Modeloids | 2022-08-30 | Paper |
Computer-Supported Analysis of Arguments in Climate Engineering | 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 |
Automating Free Logic in Isabelle/HOL | 2016-09-28 | Paper |
Agent-Based HOL Reasoning | 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 |
Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics | 2015-12-11 | Paper |
https://portal.mardi4nfdi.de/entity/Q3457212 | 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 |
PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems | 2013-12-20 | Paper |
https://portal.mardi4nfdi.de/entity/Q2847390 | 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 |
Towards computer aided mathematics | 2007-02-20 | Paper |
Computer supported mathematics with \(\Omega\)MEGA | 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 |
https://portal.mardi4nfdi.de/entity/Q2751546 | 2002-06-13 | Paper |
https://portal.mardi4nfdi.de/entity/Q2767923 | 2002-02-14 | Paper |
https://portal.mardi4nfdi.de/entity/Q2751539 | 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 |