Intelligent Computer Mathematics

by Autexier, Serge; Calmet, Jacques; Delahaye, David; Ion, Patrick D. F.; Rideau, Laurence

• ISBN13: 9783642141270
• ISBN10: 3642141277
• Format: Paperback
• Copyright: 2010-07-19
• Publisher: Springer-Verlag New York Inc
• More Book Details
• Purchase Benefits

Summary

This book constitutes the joint refereed proceedings of the 10th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2010, the 17th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2010, and the 9th International Conference on Mathematical Knowledge Management, MKM 2010.All submissions passed through a rigorous review process. From the 25 papers submitted to AISC 2010, 9 were selected for presentation at the conference and inclusion in the proceedings volume. A total of 14 papers were submitted to Calculemus, of which 7 were accepted. MKM 2010 received 27 submissions, of which 16 were accepted for presentation and publication.The events focused on the use of AI techniques within symbolic computation and the application of symbolic computation to AI problem solving; the combination of computer algebra systems and automated deduction systems; and mathematical knowledge management, respectively.

Table of Contents

Contributions to AISC 2010
The Challenges of Multivalued "Functions" (Keynote Talk)	p. 1
The Dynamic Dictionary of Mathematical Functions (Keynote Talk)	p. 13
A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence (Keynote Talk)	p. 14
I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness	p. 19
Structured Formal Development with Quotient Types in Isabelle/HOL	p. 34
Instantiation of SMT Problems Modulo Integers	p. 49
On Krawtchouk Transforms	p. 64
A Mathematical Model of the Competition between Acquired Immunity and Virus	p. 76
Some Notes upon "When Does < T > Equal Sat (T)?"	p. 89
How to Correctly Prune Tropical Trees	p. 101
From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals	p. 116
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar	p. 132
Contributions to Calculemus 2010
Some Considerations on the Usability of Interactive Provers (Invited Talk)	p. 147
Mechanized Mathematics (Invited Talk)	p. 157
Formal Proof of SCHUR Conjugate Function	p. 158
Symbolic Domain Decomposition	p. 172
A Formal Quantifier Elimination for Algebraically Closed Fields	p. 189
Computing in Coq with Infinite Algebraic Data Structures	p. 204
Formally Verified Conditions for Regularity of Interval Matrices	p. 219
Reducing Expression Size Using Rule-Based Integration	p. 234
A Unified Formal Description of Arithmetic and Set Theoretical Data Types	p. 247
Contributions to MKM 2010
Against Rigor (Invited Talk)	p. 262
Smart Matching	p. 263
Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System	p. 278
An OpenMath Content Dictionary for Tensor Concepts	p. 293
On Duplication in Mathematical Repositories	p. 300
Adapting Mathematical Domain Reasoners	p. 315
Integrating Multiple Sources to Answer Questions in Algebraic Topology	p. 331
STEXIDE: An Integrated Development Environment for STEX Collections	p. 336
Proofs, Proofs, Proofs, and Proofs	p. 345
Dimensions of Formality: A Case Study for MKM in Software Engineering	p. 355
Towards MKM in the Large: Modular Representation and Scalable Software Architecture	p. 370
The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents	p. 385
Notations Around the World: Census and Exploitation	p. 398
Evidence Algorithm and System for Automated Deduction: A Retrospective View	p. 411
On Building a Knowledge Base for Stability Theory	p. 427
Proviola: A Tool for Proof Re-animation	p. 440
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype	p. 455
Author Index	p. 471
Table of Contents provided by Ingram. All Rights Reserved.