Integrating symbolic mathematical computation and artificial intelligence : second international conference, AISMC-2, Cambridge, United Kingdom, August 3-5, 1994 : selected papers

This volume contains thoroughly revised full versions of the best papers presented at the Second International Conference on Artificial Intelligence and Sympolic Mathematical Computation, held in Cambridge, UK in August 1994. The 19 papers included give clear evidence that now, after a quite long period when AI and mathematics appeared to have arranged an amicable separation, these fields are growing together again as an area of fruitful interdisciplinary activities. This book explores the interaction between mathematical computation and clears the ground for future concentration on topics that can further unify the field. Interactive Theorem Proving And Computer Algebra / J. Ueberberg -- A Practical Algorithm For Geometric Theorem Proving / A. Rege, J. Canny -- Combining Theorem Proving And Symbolic Mathematical Computing / K. Homann, J. Calmet -- Tools For Solving Problems In The Scope Of Algebraic Programming / Y.v. Kapitonova [and Others] -- Planning A Proof Of The Intermediate Value Theorem / M. Chippendale -- A General Technique For Automatically Optimizing Programs Through The Use Of Proof Plans / P. Madden, I. Green -- Datalog And Twogroups And C++ / G. Butler -- Linear Logic And Real Closed Fields : A Way To Handle Situations Dynamically / P. Jumpertz -- A Proof Environment For Arithmetic With The Omega Rule / S. Baker, A. Smaill -- Using Commutativity Properties For Controlling Coercions / S.a. Missura, A. Weber -- Theories = Signatures + Propositions Used As Types / S.a. Missura -- The Ideal Structure Of Gröbner Base Computations / S. Collart, D. Mall -- Modeling Cooperating Agents Scenarios By Deductive Planning Methods And Logical Fiberings / J. Pfalzgraf, K. Stokkermans, U.c. Sigmund -- Propagation Of Mathematical Constraints In Subdefinite Models / V. Telerman --combining Computer Algebra And Rule Based Reasoning / R. Bündgen -- Algebraic Specification Of Empirical Inductive Learning Methods Based On Rough Sets And Matroid Theory / S. Tsumoto, H. Tanaka -- Subsymbolic Processing Using Adaptive Algorithms / D.j. Nettleton, R. Garigliano -- An Interpretation Of The Propositional Boolean Algebra As A K-algebra Effective Calculus / L.m. Laita [and Others] -- Subdefinite Computations And Symbolic Transformations In The Unicalc Solver / A. Semenov, A. Babichev, A. Leschenko. Jacques Calmet, John A. Campbell, Eds. Includes Bibliographical References. Interactive theorem proving and computer algebra....Pages 1-9 A practical algorithm for geometric theorem proving....Pages 10-17 Combining theorem proving and symbolic mathematical computing....Pages 18-29 Tools for solving problems in the scope of algebraic programming....Pages 30-47 Planning a proof of the intermediate value theorem....Pages 48-63 A general technique for automatically optimizing programs through the use of proof plans....Pages 64-79 Datalog and TwoGroups and C++....Pages 80-92 Linear logic and real closed fields: A way to handle situations dynamically....Pages 93-114 A proof environment for arithmetic with the omega rule....Pages 115-130 Using commutativity properties for controlling coercions....Pages 131-143 Theories = signatures + propositions used as types....Pages 144-155 The ideal structure of Gröbner base computations....Pages 156-166 Modeling cooperating agents scenarios by deductive planning methods and logical fiberings....Pages 167-190 Propagation of mathematical constraints in subdefinite models....Pages 191-208 Combining computer algebra and rule based reasoning....Pages 209-223 Algebraic specification of empirical inductive learning methods based on rough sets and matroid theory....Pages 224-243 Subsymbolic processing using adaptive algorithms....Pages 244-254 An interpretation of the propositional Boolean algebra as a k-algebra. Effective calculus....Pages 255-263 Subdefinite computations and symbolic transformations in the uniCalc solver....Pages 264-275 This volume contains versions of selected papers presented at the Second Artificial Intelligence and Sympolic Mathematical Computation, held in Cambridge, 1994. It explores the interaction between mathematical computation and indicates further topics that may be concentrated upon. Interactive Theorem Proving, ITP for short, is a new approach for the use of current computer algebra systems to support mathematicians in proving theorems.