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: Lecture Notes in Computer Science, cartea 6167

Editat de Serge Autexier, Jacques Calmet, David Delahaye, P.D.F. Ion, Laurence Rideau, Renaud Rioboo, Alan Sexton
en Limba Engleză Paperback – 30 iun 2010

Din seria Lecture Notes in Computer Science

Preț: 35850 lei

Puncte Express: 538

Preț estimativ în valută:
6860 7331$ 5770£

Carte disponibilă

Livrare economică 08-22 iulie

Preluare comenzi: 021 569.72.76


ISBN-13: 9783642141270
ISBN-10: 3642141277
Pagini: 486
Ilustrații: XV, 471 p. 71 illus.
Greutate: 0.73 kg
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Lecture Notes in Artificial Intelligence

Locul publicării:Berlin, Heidelberg, Germany

Public țintă



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.


Up-to-date results