KLUEDO | Suchen

Mechanization of Strong Kleene Logic for Partial Functions (1999)

Manfred Kerber Michael Kohlhase

Even though it is not very often admitted, partial functions do play asignificant role in many practical applications of deduction systems. Kleenehas already given a semantic account of partial functions using three-valuedlogic decades ago, but there has not been a satisfactory mechanization. Recentyears have seen a thorough investigation of the framework of many-valuedtruth-functional logics. However, strong Kleene logic, where quantificationis restricted and therefore not truth-functional, does not fit the frameworkdirectly. We solve this problem by applying recent methods from sorted logics.This paper presents a resolution calculus that combines the proper treatmentof partial functions with the efficiency of sorted calculi.

Adaptation of Declaratively Represented Methods in Proof Planning (1999)

Xiaorong Huang Manfred Kerber Lassaad Cheikhrouhou

The reasoning power of human-oriented plan-based reasoning systems is primarilyderived from their domain-specific problem solving knowledge. Such knowledge is, how-ever, intrinsically incomplete. In order to model the human ability of adapting existingmethods to new situations we present in this work a declarative approach for represent-ing methods, which can be adapted by so-called meta-methods. Since apparently thesuccess of this approach relies on the existence of general and strong meta-methods,we describe several meta-methods of general interest in detail by presenting the prob-lem solving process of two familiar classes of mathematical problems. These examplesshould illustrate our philosophy of proof planning as well: besides planning with thecurrent repertoire of methods, the repertoire of methods evolves with experience inthat new ones are created by meta-methods which modify existing ones.

Proving Ground Completeness of Resolution by Proof Planning (1999)

Manfred Kerber Arthur C. Sehn

A lot of the human ability to prove hard mathematical theorems can be ascribedto a problem-specific problem solving know-how. Such knowledge is intrinsicallyincomplete. In order to prove related problems human mathematicians, however,can go beyond the acquired knowledge by adapting their know-how to new relatedproblems. These two aspects, having rich experience and extending it by need, can besimulated in a proof planning framework: the problem-specific reasoning knowledge isrepresented in form of declarative planning operators, called methods; since these aredeclarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs intheorem proving, first, we present methods for proving the ground completeness ofbinary resolution, which essentially correspond to key lemmata, and then, we showhow these methods can be reused for the proof of the ground completeness of lockresolution.

An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs (1999)

Manfred Kerber Michael Kohlhase Volker Sorge

Mechanised reasoning systems and computer algebra systems have apparentlydifferent objectives. Their integration is, however, highly desirable, since in manyformal proofs both of the two different tasks, proving and calculating, have to beperformed. Even more importantly, proof and computation are often interwoven andnot easily separable. In the context of producing reliable proofs, the question howto ensure correctness when integrating a computer algebra system into a mechanisedreasoning system is crucial. In this contribution, we discuss the correctness prob-lems that arise from such an integration and advocate an approach in which thecalculations of the computer algebra system are checked at the calculus level of themechanised reasoning system. This can be achieved by adding a verbose mode to thecomputer algebra system which produces high-level protocol information that can beprocessed by an interface to derive proof plans. Such a proof plan in turn can beexpanded to proofs at different levels of abstraction, so the approach is well-suited forproducing a high-level verbalised explication as well as for a low-level machine check-able calculus-level proof. We present an implementation of our ideas and exemplifythem using an automatically solved extended example.

Useful Properties of a Frame-Based Representation of Mathematical Knowledge (1999)

Manfred Kerber

To prove difficult theorems in a mathematical field requires substantial know-ledge of that field. In this paper a frame-based knowledge representation formalismis presented, which supports a conceptual representation and to a large extent guar-antees the consistency of the built-up knowledge bases. We define a semantics ofthe representation by giving a translation into the underlaying logic.

A Mathematical Knowledge Base for Proving Theorems in Semigroup and Automata Theory (1999)

Barbara Schütt Manfred Kerber

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.

Omega: Towards a Mathematical Assistant (1999)

Christoph Benzmüller Lassaad Cheikhrouhou Detlef Fehrer Armin Fiedler Xiaorong Huang Manfred Kerber Michael Kohlhase Karsten Konrad Andreas Meier

-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.

Specifying and Reasoning about Generic Real-Time Requirements - A Case Study (1999)

Reinhard Gotzhein Martin Kronenburg Christian Peper

A non-trivial real-time requirement obeying a pattern that can be foundin various instantiations in the application domain building automation, and which is therefore called generic, is investigated in detail. Starting point is a description of a real-time problem in natural language augmented by a diagram, in a style often found in requirements documents. Step by step, this description is made more precise and finally transformed into a surprisingly concise formal specification, written in real-time temporal logic with customized operators. Wereason why this formal specification precisely captures the original description- as far as this is feasible due to the lack of precision of natural language.

Boltzmann Simulation by Particle Methods (1994)

Helmut Neunzert Jens Struckmeier

Particle methods to simulate rarefied gas flows have found an increasing interest in Computational Fluid Dynamics during the last decade, see for example [1], [2], [3] and [4]. The general goal is to develop numerical schemes which are reliable enough to substitute real windtunnel experiments, needed for example in space research, by computer experiments. In order to achieve this goal one needs numerical methods solving the Boltzmann equation including all important physical effects. In general this means 3D computations for a chemically reacting rarefied gas. With codes of this kind at hand, Boltzmann simulation becomes a powerful tool in studying rarefied gas phenomena.

Classification of Location Problems (1999)

Horst W. Hamacher Stefan Nickel Anja Schneider

There are several good reasons to introduce classification schemes for optimization problems including, for instance, the ability for concise problem statement opposed to verbal, often ambiguous, descriptions or simple data encoding and information retrieval in bibliographical information systems or software libraries. In some branches like scheduling and queuing theory classification is therefore a widely accepted and appreciated tool. The aim of this paper is to propose a 5-position classification which can be used to cover all location problems. We will provide a list of currentliy available symbols and indicate its usefulness in a - necessarily non-comprehensive - list of classical location problems. The classification scheme is in use since 1992 and has since proved to be useful in research, software development, classroom, and for overview articles.

Filtern

Fachbereich / Organisatorische Einheit

Autor

Erscheinungsjahr

Dokumenttyp

Sprache

Volltext vorhanden

Schlagworte

2241 Treffer