Intelligent Computer Mathematics 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings
| Other Authors: | , , , |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
2010, 2010
|
| Edition: | 1st ed. 2010 |
| Series: | Lecture Notes in Artificial Intelligence
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- Contributions to AISC 2010
- The Challenges of Multivalued “Functions”
- The Dynamic Dictionary of Mathematical Functions
- A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence
- I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness
- Structured Formal Development with Quotient Types in Isabelle/HOL
- Instantiation of SMT Problems Modulo Integers
- On Krawtchouk Transforms
- A Mathematical Model of the Competition between Acquired Immunity and Virus
- Some Notes upon “When Does $]]> Equal Sat ?”
- How to Correctly Prune Tropical Trees
- From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- Contributions to Calculemus 2010
- Some Considerations on the Usability of Interactive Provers
- Mechanized Mathematics
- Formal Proof of SCHUR Conjugate Function
- The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents
- Notations Around the World: Census and Exploitation
- Evidence Algorithm and System for Automated Deduction: A Retrospective View
- On Building a Knowledge Base for Stability Theory
- Proviola: A Tool for Proof Re-animation
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- Symbolic Domain Decomposition
- A Formal Quantifier Elimination for Algebraically Closed Fields
- Computing in Coq with Infinite Algebraic Data Structures
- Formally Verified Conditions for Regularity of Interval Matrices
- Reducing Expression Size Using Rule-Based Integration
- A Unified Formal Description of Arithmetic and Set Theoretical Data Types
- Contributions to MKM 2010
- Against Rigor
- Smart Matching
- Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System
- An OpenMath Content Dictionary for Tensor Concepts
- On Duplication in Mathematical Repositories
- Adapting Mathematical Domain Reasoners
- Integrating Multiple Sources to Answer Questions in Algebraic Topology
- An Integrated Development Environment for Collections
- Proofs, Proofs, Proofs, and Proofs
- Dimensions ofFormality: A Case Study for MKM in Software Engineering
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture