Skip to main content
main-content

Über dieses Buch

This book is a collection of selected papers written by researchers qf our "RISC" institute (Research Institute for Symbolic Computation) along with the ESPRIT MEDLAR Project (Mechanizing Deduction in the Logics of Practical Reason­ ing). Naturally, the MEDLAR Project was and is the focal point for our institute whose main objective is the combination of foundational research in the area of symbolic computation and possible applications thereof for high-tech industrial projects. I am grateful to the director of the MEDLAR project, Jim Cunningham, for his enthusiasm, profound expertise, and continuous effort to manage a fruitful cooperation between various European working groups in the area of the project and for giving us the opportunity to be part of this challenging endeavor. I also acknowledge and feel indebted to Jochen Pfalzgraf for managing the RISC part of the MEDLAR project and to both him and Dongming Wang for editing this volume and organizing the refereeing process.

Inhaltsverzeichnis

Frontmatter

Introduction

Abstract
This book presents a collection of articles with topics linked to the working areas of a project named MEDLAR in which both the editors are actively involved. The authors of all the contributions are currently working or worked at the Research Institute for Symbolic Computation, Johannes Kepler University Linz (RISC-Linz).
Jochen Pfalzgraf, Dongming Wang

An Algorithm for Solving Systems of Algebraic Equations in Three Variables

Abstract
The most famous algorithm for computing the greatest common divisor (gcd) of two univariate polynomials over a field is, undoubtedly, the algorithm of Euclid. In attempting to generalize it to the multivariate case one easily arrives at the concept of polynomial remainder sequences and discovers the phenomenon of explosive coefficient growth (see, e.g., Brown 1971). To overcome this problem primitive polynomial remainder sequences (pprs) have been introduced. However, the classical primitive polynomial remainder sequence algorithm for computing gcds (Brown 1971) has one rather obvious disadvantage. In order to make a polynomial primitive, its content, which is the gcd of its coefficients, has to be computed. Therefore, additional gcd computations in the coefficient domain are necessary for computing a pprs. Fortunately, the costs of these content computations can be considerably reduced by subresultant techniques (Collins 1967, Brown and Traub 1971, Brown 1978) or trial division (Hearn 1979, Stoutemyer 1985).
Michael Kalkbrener

On a General Notion of a Hull

Abstract
In this contribution we give a short presentation of ongoing work in the areas of the general framework and mathematical foundations in MEDLAR II. Our objective is to sketch a brief survey of the problems, the methods and existing results and we conclude with prospects of work in progress. We start with some background information and motivational remarks which form the basis of the subsequent considerations. As mentioned in the following, joint article with K. Stokkermans the logical fiberings (as introduced in Pfalzgraf 1991) provide semantical models for indexed systems of logics and they have (semantical) links to D. Gabbay’s extensive theory of labelled deductive systems (LDS). He sees the logical fiberings as a (general) semantics for LDS and introduced the notion of “fibered semantics.” The LDS form a general framework for the great challenge of “putting logics together” in an integrated system (cf. Gabbay 1990, 1994a, b). This indicates the central interest of fibered structures concerning a general semantics modeling approach. Compare the “sheaf semantics” arising naturally in our subsequent considerations.
Jochen Pfalzgraf

On Robotics Scenarios and Modeling with Fibered Structures

Abstract
The field of robotics has been one of the main working areas of the RISC-Linz group in the MEDLAR project. In the first project year of BRA 3125 (subsequently referred to as MEDLAR I) we started with case studies (Pfalzgraf and Stokkermans 1992) in order to get an overview of material which we considered to be relevant as support and motivation of future project work. These future aspects are especially seen with regard to the applications of methods developed by the other project partners. Therefore it became more and more clear that one of the main objectives of our work on robotics has to do with the construction of “scenarios” where various reasoning methods can be applied and tested and extended. That means that we thought of providing testbeds where each partner should be able to identify a problem suitable for application of her/his corresponding methods, respectively. This would describe the ideal case. Subsequently, in the next section, we will go into more details. Actually, the development of these ideas started in the course of MEDLAR I and they found enough interest as to be continued in the first year of MEDLAR II (BRP 6471), the project successor of MEDLAR I. The existing material is intended to serve as a basis for work on parts of a MEDLAR practical reasoner (in the third year). In our case this refers to a reasoning module for specific robotics problems which corresponds to our special fields of interest namely algebraic approaches to geometric reasoning problems with emphasis on robot kinematics and singularity problems.
Jochen Pfalzgraf, Karel Stokkermans

On Algorithmic Parametrization Methods in Algebraic Geometry

Abstract
The parametrization problem can be described as the problem of finding a general closed form solution to a system of algebraic equations, where “closed form” means rational functions in one or more free parameters.
Josef Schicho

Towards a Categorical Calculus for Critical-Pair/Completion

Abstract
The ultimate aim of the research reported here is to provide a general framework for algorithms that show the following two characteristics: critical pairs and completion. Here completion means extending a certain set of reductions (given by, e.g., rewrite rules, or polynomials from an ideal) until that set fulfills some completeness property. Critical pairs are used for the selection of elements for which the reduction relation to be completed is not yet confluent. The selection is essentially done by superposing left hand sides of basic reduction rules, and testing whether applying the applicable reduction rules yield the same reducts. If not, one forces confluence by adding a reduction rule between the differing reducts (if possible without violating certain conditions on the reduction relation).
Karel Stokkermans

CASA: Computer Algebra Software for Computing with Algebraic Sets

Abstract
In this report we want to illustrate with two examples how the program package “Computer Algebra Software for Constructive Algebraic Geometry” (CASA) (see Gebauer et al. 1991) can be used in order to reason about geometric objects defined by algebraic equations.
Bernhard Wall

Reasoning about Geometric Problems using an Elimination Method

Abstract
The present work relates to a paper by (1991) in which he explained the reasoning about a set of selected, geometry-related problems by using the algebraic methods of characteristic sets (Ritt 1950; Wu 1984a, b), Gröbner bases (Buchberger 1985) and cylindrical algebraic decomposition (Collins 1975). Its main purpose is to demonstrate how to deal with the same set of geometric problems by using another algebraic method which is based on some elimination procedures proposed by (1993). We use the same formulations of the problems (with slight modifications when necessary) and the same set of illustrative examples given previously (Wang 1991). It is shown that for most of the examples our new method takes less computing time than the methods of characteristic sets and Gröbner bases do.
Dongming Wang

An Implementation of the Characteristic Set Method in Maple

Abstract
The method of characteristic sets was introduced by J. F. Ritt (1932, 1950) in the context of his work on differential algebra in the early 1930s and was revitalized and further developed by Wen-tsün Wu (1984a, b, 1986) through his recent work on mathematics-mechanization. In addition to being a powerful tool for Wu’s general theory and method of mechanical theorem proving, the characteristic set method has proved efficient for solving a wide class of problems in geometry and algebra (see the series of work in “Mathematics-Mechanization Research Preprints” 1–11, 1987–1994, for example). It has been partially implemented by different research groups in China, USA and Austria (Chou 1988, Ko 1986, Kusche et al. 1989) for geometry theorem proving and solving other relevant problems. The author has learned that an implementation of this method in the Reduce system is ongoing at the University of Bath, England. However, to the best of our knowledge neither a complete implementation exists nor a partial implementation has been generally available in current symbolic and algebraic computation systems. The incompleteness of the existing implementations was mainly due to difficulties in polynomial factorization over successive algebraic extension fields (for which there was a lack of general and efficient procedures) and the determination of prime bases of ideals from their characteristic sets (for which no simple and practical method was available). We have overcome the difficulties through the discovery of a new method for polynomial factorization and the application of Gröbner bases for determining the prime bases.
Dongming Wang

A Nonmonotonic Extension to Horn-Clause Logic

Abstract
Standard first-order logic, and therefore, any description of the world that relies on it, ordinarily requires the absence of contradiction. It has been repeatedly pointed out that in describing the real world it is often very difficult to avoid making contradictory statements (e.g., when realizing that an assumption had proven wrong, we might have to assert the denial of what we had assumed to hold true). The example that has become a classic in the AI literature is the problem that Birds fly, Penguins are birds, but Penguins don’t fly.
Thomas J. Weigert

Backmatter

Weitere Informationen