-
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.
-
13Natural 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.
-
142Quantified Multimodal Logics in Simple Type TheoryLogica Universalis 7 (1): 7-20. 2013.We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory
-
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.
-
9Integrating 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
-
38Multimodal and intuitionistic logics in simple type theoryLogic Journal of the IGPL 18 (6): 881-892. 2010.We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II
-
191Higher-Order Semantics and ExtensionalityJournal of Symbolic Logic 69 (4). 2004.In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-ord…Read more
-
14Embedding and Automating Conditional Logics in Classical Higher-Order LogicAnnals of Mathematics and Artificial Intelligence 66 (1-4): 257-271. 2012.
-
106Comparing Approaches To Resolution Based Higher-Order Theorem ProvingSynthese 133 (1-2): 203-335. 2002.We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratet…Read more
-
39Cut-Elimination for Quantified Conditional LogicJournal of Philosophical Logic 46 (3): 333-353. 2017.A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.
-
23Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order LogicAnnals of Mathematics and Artificial Intelligence) 62 (1-2): 103-128. 2011.
-
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
-
18Agent based Mathematical ReasoningElectronic Notes in Theoretical Computer Science, Elsevier 23 (3): 21-33. 1999.In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means finished. We present and discuss our proposal in order to get feedback from the Calculemus community.
-
65Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automate…Read more
-
17Assertion-level Proof Representation with Under-SpecificationElectronic Notes in Theoretical Computer Science 93 5-23. 2004.
-
12Organisation, Transformation, and Propagation of Mathematical Knowledge in OmegaMathematics in Computer Science 2 (2): 253-277. 2008.
-
10Preface: Proceedings of the 8th Workshop on User Interfaces for Theorem ProversElectronic Notes in Theoretical Computer Science 226 (1): 1-2. 2009.
-
102Higher-order semantics and extensionalityJournal of Symbolic Logic 69 (4): 1027-1088. 2004.In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods needed to analyze completeness of higher-order calculi with respect to these model classes
-
676Computers may help us to better understand (not just verify) arguments. In this article we defend this claim by showcasing the application of a new, computer-assisted interpretive method to an exemplary natural-language ar- gument with strong ties to metaphysics and religion: E. J. Lowe’s modern variant of St. Anselm’s ontological argument for the existence of God. Our new method, which we call computational hermeneutics, has been particularly conceived for use in interactive-automated proof ass…Read more
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology |
Science, Logic, and Mathematics |
Areas of Interest
Metaphysics and Epistemology |
Science, Logic, and Mathematics |