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 /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Autexier, Serge (Επιμελητής έκδοσης), Calmet, Jacques (Επιμελητής έκδοσης), Delahaye, David (Επιμελητής έκδοσης), Ion, Patrick D. F. (Επιμελητής έκδοσης), Rideau, Laurence (Επιμελητής έκδοσης), Rioboo, Renaud (Επιμελητής έκδοσης), Sexton, Alan P. (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2010.
Σειρά:Lecture Notes in Computer Science, 6167
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • 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
  • 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 of Formality: A Case Study for MKM in Software Engineering
  • Towards MKM in the Large: Modular Representation and Scalable Software Architecture
  • 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.