Catálogo de publicaciones - libros

We provide a theoretical framework that allows the direct search for natural deduction proofs in some non-classical logics, namely, intuitionistic sentential and predicate logic, but also in the modal logic S4. The framework uses so-called intercalation calculi to build up broad search spaces from which normal proofs can be extracted, if a proof exists at all. This claim is supported by completeness proofs establishing in a purely semantic way normal form theorems for the above logics. Logical restrictions on the search spaces are briefly discussed in the last section together with some heuristics for structuring a more efficient search. Our paper is a companion piece to [15], where classical logic was treated.

In this survey on implicit induction I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem proving, esp. memories that significantly differ from the presentation in a recent handbook article on “inductionless induction”. Moreover, the important references excluded there are provided here. In order to clear the fog a little, there is a short introduction to inductive theorem proving and a discussion of connotations of implicit induction like “”, “inductionless induction”, “proof by consistency”, implicit induction orderings (term orderings), and refutational completeness.

This article celebrates with obvious joy the role automated reasoning now plays for mathematics and logic. Simultaneously, this article evidences the realization of a dream thought impossible just four decades ago by almost all. But there were believers, including Joerg Siekmann to whom this article is dedicated in honor of his sixtieth birthday. Indeed, today (in the year 2001) a researcher can enlist the aid of an automated reasoning program often with the reward of a new proof or a better proof in some significant aspect. The contributions to mathematics and logic made with an automated reasoning assistant are many, diverse, often significant, and of the type Hilbert would indeed have found most pleasurable. The proofs discovered by W. McCune’s OTTER (as well as other programs) are Hilbert-style axiomatic. Further, some of them address Hilbert’s twenty-fourth problem (recently unearthed by Rudiger Thiele), which focuses on the completion of simpler proofs. In that regard, as well as others, I offer challenges and open questions, frequently providing appropriate clauses to provide a beginning.

The vision of a Semantic Web has recently drawn considerable attention, both from academia and industry. Description logics are often named as one of the tools that can support the Semantic Web and thus help to make this vision reality.

In this paper, we describe what description logics are and what they can do for the Semantic Web. Descriptions logics are very useful for defining, integrating, and maintaining ontologies, which provide the Semantic Web with a common understanding of the basic semantic concepts used to annotate Web pages. We also argue that, without the last decade of basic research in this area, description logics could not play such an important rôle in this domain.

This work is about a “real-world” application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. These documents are “living”, in the sense, that they can be modified and extended by the reader, who can interact via Living Books with external systems.

A particular task is to assemble a new document from such units in a selective way, based on the user’s current interest and knowledge.

It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism.

This is a light ‘divertissement’ about the problems of modern transportation, and the beckoning pleasures of meeting with Jörg.

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 to adjust for a particular theorem prover. Only recently there have been initiatives to flexibly connect existing theorem proving systems into networked environments that contain large knowledge bases. An intermediate layer containing both, search and proving functionality can be used to mediate between the two.

In this paper we motivate the need and discuss the requirements for mediators between mathematical knowledge bases and theorem proving systems. We also present an attempt at a concurrent mediator between a knowledge base and a proof planning system.

In this paper we present a Head-driven Phrase Structure Grammar (HPSG) grammar of Polish – the result of one of the few attempts (e.g., [Szp86], [Świ92]) to build formal and computationally tractable grammars of Polish. The choice of the formalism used was motivated by several promising features of the formalism which we will present shortly.

Schematic proofs are functions which can produce a proof of a proposition for each value of their parameters. A schematic proof can be constructed by abstracting a general pattern of proof from several examples of a family of proofs. In this paper we examine several interesting aspects of the use of schematic proofs in mathematics. Furthermore, we pose several conjectures about the psychological validity of the use of schematic proofs in mathematics. These conjectures need testing, hence we propose an empirical study which would either support or refute our conjectures. Ultimately, we suggest that schematic proofs are worthy of a closer and more detailed study and investigation.

State-of-the-art proof presentation systems suffer from several deficiencies. First, they simply present the proofs without motivating why the proof is done as it is done. Second, they neglect the issue of user modeling and thus forgo the ability to adapt the presentation to the specific user. Finally, they do not allow the user to interact with the system to ask questions about the proof.

As a first step to overcome these deficiencies, we developed a computational model of user-adaptive proof explanation, which is implemented in a generic, user-adaptive proof explanation system, called (for ). To do so, we used techniques from three different fields, namely from computational logic to represent proofs ensuring the correctness; from cognitive science to model the users mathematical knowledge and skills; and from natural language processing to plan the explanation of the proofs and to react to the user’s interactions.