Automated Practical Reasoning

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

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

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.

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.

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.

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

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.

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.

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.

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.