-
17Assertion-level Proof Representation with Under-SpecificationElectronic Notes in Theoretical Computer Science 93 5-23. 2004.
-
16Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order LogicLogic and Logical Philosophy 25 (4): 535-554. 2016.
-
16Embedding and Automating Conditional Logics in Classical Higher-Order LogicAnnals of Mathematics and Artificial Intelligence 66 (1-4): 257-271. 2012.
-
14Natural Language Dialog with a Tutor System for Mathematical ProofsIn Ruqian Lu, Jörg Siekmann & Carsten Ullrich (eds.), Cognitive Systems: Joint Chinese-German Workshop, Shanghai, China, March 7-11, 2005, Revised Selected Papers, Springer. pp. 1-14. 2007.
-
13Verifying the Modal Logic Cube is an Easy TaskIn Simon Siegler & Nathan Wasser (eds.), Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, Springer. pp. 117-128. 2010.
-
13Bridging Theorem Proving and Mathematical Knowledge RetrievalIn Dieter Hutter (ed.), Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday, Springer. pp. 277-296. 2004.Accessing knowledge of a single knowledge source with different client applications often requires the help of mediator systems as middleware components. In the domain of theorem proving large efforts have been made to formalize knowledge for mathematics and verification issues, and to structure it in databases. But these databases are either specialized for a single client, or if the knowledge is stored in a general database, the services this database can provide are usually limited and hard t…Read more
-
13Interactive Theorem Proving with TasksElectronic Notes in Theoretical Computer Science 103 (C): 161-181. 2004.
-
12Integrating TPS and OMEGAJournal of Universal Computer Science 5 (3): 188-207. 1999.This paper reports on the integration of the higher-order theorem proving environment TPS [Andrews96] into the mathematical assistant OMEGA [Omega97]. TPS can be called from OMEGA either as a black box or as an interactive system. In black box mode, the user has control over the parameters which control proof search in TPS; in interactive mode, all features of the TPS-system are available to the user. If the subproblem which is passed to TPS contains concepts defined in OMEGA’s database of mathe…Read more
-
12Organisation, Transformation, and Propagation of Mathematical Knowledge in OmegaMathematics in Computer Science 2 (2): 253-277. 2008.
-
10A Simplified Variant of Gödel’s Ontological ArgumentIn Vestrucci Andrea (ed.), Beyond Babel: Religion and Linguistic Pluralism, Springer Verlag. pp. 271-286. 2023.A simplified variant of Gödel’s ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments wa…Read more
-
10Preface: Proceedings of the 8th Workshop on User Interfaces for Theorem ProversElectronic Notes in Theoretical Computer Science 226 (1): 1-2. 2009.
-
8On Gödel and the Nonexistence of Time – Gödel und die Nichtexistenz der Zeit: Kurt Gödel essay competition 2021 – Kurt-Gödel-Preis 2021 (edited book)Springer Berlin Heidelberg. 2023.
-
7The curious inference of Boolos in MIZAR and OMEGAIn Matuszewski Roman & Zalewska Anna (eds.), From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec, The University of Bialystok, Polen. pp. 299-388. 2007.
-
3Who Finds the Short Proof?Logic Journal of the IGPL. forthcoming.This paper reports on an exploration of Boolos’ Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos’ and related examples now seems to be within reach of higher-order ATPs.
-
Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India (edited book)The Bhaktivedanta Institute. 2018.
-
Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22 (edited book)Springer. 2021.
-
Reasoning in simple type theory — Festschrift in honor of Peter B. Andrews on his 70th birthday, Studies in Logic, vol. 17 (review)Bulletin of Symbolic Logic 16 (3): 409-411. 2010.
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology |
Science, Logic, and Mathematics |
Areas of Interest
Metaphysics and Epistemology |
Science, Logic, and Mathematics |