Automated Practical Reasoning

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.

Contenu

An algorithm for solving systems of algebraic equations in three variables.- 1 Introduction.- 2 Definitions.- 3 Basic properties of primitive polynomial remainder sequences and elimination sequences.- 4 Application of elimination sequences: solution of systems of algebraic equations.- 5 Systems of algebraic equations in two variables.- 6 Systems of algebraic equations in three variables.- 7 Applications in neural networks theory.- References.- On a general notion of a hull.- 1 Introduction.- 2 Basic notions.- 3 General relational structures.- 4 Some examples.- 5 Prospects.- 6 Concluding remarks.- References.- On robotics scenarios and modeling with fibered structures.- 1 Introduction.- 2 Motivational remarks and background.- 3 Description of the first subscenario.- 4 The logical fibering model.- 5 A proposed model of the general state space of an agent.- 6 Subscenario with autonomous agents.- 7 Conclusion.- References.- On algorithmic parametrization methods in algebraic geometry.- 1 Introduction.- 2 Rational and unirational varieties.- 3 Curves.- 4 Surfaces.- 5 Higher dimensional varieties.- References.- Towards a categorical calculus for critical-pair/completion.- 1 Introduction.- 2 Overview of CPC-procedures.- 3 An axiomatic framework.- 4 A little category theory.- 5 Reversed limits.- 6 A categorical model for CPC-procedures.- References.- CASA: computer algebra software for computing with algebraic sets.- 1 Introduction.- 2 Intersection of algebraic sets - a case study.- 3 Puiseux expansion in CASA.- References.- Reasoning about geometric problems using an elimination method.- 1 Introduction.- 2 An elimination method for polynomial systems.- 3 Mechanical geometry theorem proving.- 4 Automatic derivation of unknown relations.- 5 Automatic derivation of locus equations.- 6 Implicitization of parametric objects.- 7 Existence conditions and detection of singularities.- 8 Decomposition of algebraic varieties.- 9 Inverse robot kinematics.- 10 Intersection of geometric objects.- References.- An implementation of the characteristic set method in Maple.- 1 Introduction and notations.- 2 Description of user functions.- 3 Modifications and strategies.- 4 Test results and remarks.- Appendix: Test problems.- References.- A nonmonotonic extension to Horn-clause logic.- 1 Introduction.- 2 Semantics of nonmonotonic Horn-clause theories.- 3 Soundness and completeness of nonmonotonic Horn-clause theories.- 4 Relationship to model-theoretic semantics.- 5 Conclusion.- References.