KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Mon, 03 Apr 2000 00:00:00 +0200Mon, 03 Apr 2000 00:00:00 +0200A Mathematical Knowledge Base for Proving Theorems in Semigroup and Automata Theory
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/424
We present a mathematical knowledge base containing the factual know-ledge of the first of three parts of a textbook on semi-groups and automata,namely "P. Deussen: Halbgruppen und Automaten". Like almost all math-ematical textbooks this textbook is not self-contained, but there are somealgebraic and set-theoretical concepts not being explained. These concepts areadded to the knowledge base. Furthermore there is knowledge about the nat-ural numbers, which is formalized following the first paragraph of "E. Landau:Grundlagen der Analysis".The data base is written in a sorted higher-order logic, a variant of POST ,the working language of the proof development environment OmegaGamma mkrp. We dis-tinguish three different types of knowledge: axioms, definitions, and theorems.Up to now, there are only 2 axioms (natural numbers and cardinality), 149definitions (like that for a semi-group), and 165 theorems. The consistency ofsuch knowledge bases cannot be proved in general, but inconsistencies may beimported only by the axioms. Definitions and theorems should not lead to anyinconsistency since definitions form conservative extensions and theorems areproved to be consequences.Barbara Schütt; Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/424Mon, 03 Apr 2000 00:00:00 +0200Omega: Towards a Mathematical Assistant
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/428
-mega is a mixed-initiative system with the ultimate pur-pose of supporting theorem proving in main-stream mathematics andmathematics education. The current system consists of a proof plannerand an integrated collection of tools for formulating problems, provingsubproblems, and proof presentation.Christoph Benzmüller; Lassaad Cheikhrouhou; Detlef Fehrer; Armin Fiedler; Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Karsten Konrad; Andreas Meierpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/428Mon, 03 Apr 2000 00:00:00 +0200