Serge Autexier

Intelligent Computer Mathematics - Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence Serge Autexier

Marc Notes: Includes bibliographical references and index.; Avail. in electronic form. Table of Contents: Contributions to AISC 2010 -- The Challenges of Multivalued Functions (Keynote Talk) / James H. Davenport -- The Dynamic Dictionary of Mathematical Functions (Keynote Talk) / Bruno Salvy -- A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence (Keynote Talk) / Jacques Calmet, John A. Campbell -- I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness / Hicham Bensaid, Ricardo Caferra, Nicolas Peltier -- Structured Formal Development with Quotient Types in Isabelle/HOL / Maksym Bortin, Christoph LUth -- Instantiation of SMT Problems Modulo Integers / Mnacho Echenim, Nicolas Peltier -- On Krawtchouk Transforms / Philip Feinsilver, RenE Schott -- A Mathematical Model of the Competition between Acquired Immunity and Virus / Mikhail K. Kolev -- Some Notes upon When Does Equal Sat (T)? / Yongbin Li -- How to Correctly Prune Tropical Trees / Jean-Vincent Loddo, Luca Saiu -- From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals / Salvador Lucas -- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar / Josef Urban, Geoff Sutcliffe -- Contributions to Calculemus 2010 -- Some Considerations on the Usability of Interactive Provers (Invited Talk) / Andrea Asperti, Claudio Sacerdoti Coen -- Mechanized Mathematics (Invited Talk) / Jacques Carette -- Formal Proof of SCHUR Conjugate Function / Franck Butelle, Florent Hivert, Micaela Mayero, FrEdEric Toumazet -- Symbolic Domain Decomposition / Jacques Carette, Alan P. Sexton, Volker Sorge, Stephen M. Watt -- A Formal Quantifier Elimination for Algebraically Closed Fields / Cyril Cohen, Assia Mahboubi -- Computing in Coq with Infinite Algebraic Data Structures / CEsar DomInguez, Julio Rubio -- Formally Verified Conditions for Regularity of Interval Matrices / Ioana Pasca -- Reducing Expression Size Using Rule-Based Integration / David J. Jeffrey, Albert D. Rich -- A Unified Formal Description of Arithmetic and Set Theoretical Data Types / Paul Tarau -- Contributions to MKM 2010 -- Against Rigor (Invited Talk) / Doron Zeilberger -- Smart Matching / Andrea Asperti, Enrico Tassi -- Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System / Xiaoyu Chen -- An OpenMath Content Dictionary for Tensor Concepts / Joseph B. Collins -- On Duplication in Mathematical Repositories / Adam Grabowski, Christoph Schwarzweller -- Adapting Mathematical Domain Reasoners / Bastiaan Heeren, Johan Jeuring -- Integrating Multiple Sources to Answer Questions in Algebraic Topology / JOnathan Heras, Vico Pascual, Ana Romero, Julio Rubio -- STEXIDE: An Integrated Development Environment for STEX Collections / Constantin Jucovschi, Michael Kohlhase -- Proofs, Proofs, Proofs, and Proofs / Manfred Kerber -- Dimensions of Formality: A Case Study for MKM in Software Engineering / Andrea Kohlhase, Michael Kohlhase, Christoph Lange -- Towards MKM in the Large: Modular Representation and Scalable Software Architecture / Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev -- The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents / Andriy Kovalchuk, Vyachelav Levitsky, Igor Samolyuk, Valentyn Yanchuk -- Notations Around the World: Census and Exploitation / Paul Libbrecht -- Evidence Algorithm and System for Automated Deduction: A Retrospective View / Alexander Lyaletski, Konstantin Verchinine -- On Building a Knowledge Base for Stability Theory / Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller -- Proviola: A Tool for Proof Re-animation / Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk -- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype / Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers -- Author Index. Publisher Marketing: Thisvolumecontainsthecollectedcontributionsofthreeconferences, AISC2010, Calculemus 2010 and MKM 2010. AISC 2010 was the 10th International C- ference on Arti?cial Intelligence and symbolic computation. Its area of concern is the use of AI techniques within symbolic computation as well as the appli- tion of symbolic computation to AI problem solving. Calculemus 2010 was the 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, dedicated to the combination of computer algebra systems and - tomated deduction systems. MKM 2010 was the 9th International Conference on Mathematical KnowledgeManagement, an emerging interdisciplinary?eld of research in the intersection of mathematics, computer science, library science, andscienti?cpublishing. Allthreeconferencesarethusconcernedwithproviding intelligent computer mathematics. Although the conferences have separate c- munities and separate foci, there is a signi?cant overlap of interest in building systems for intelligent computer mathematics. As in 2008 and 2009, the three events were colocated. In 2010 this was at the Conservatoire National des Arts et M etiers (CNAM), Paris, France, under the umbrellaoftheConferencesonIntelligentComputerMathematics(CICM2010), organized by Renaud Rioboo and Laurence Rideau. This collocation is intended to counteract the tendency towards fragmentation of communities working on di?erent aspects of various independent branchesof our general?eld; traditional branches (e. g., computer algebra, theorem proving and arti?cial intelligence in general), as well as newly emerging ones (on user interfaces, knowledge mana- ment, theory exploration, etc. ). This also facilitates the development of systems for intelligent computer mathematics that will be routinely used by mathema- cians, computer scientists and engineers in their every-day work."