Cantitate/Preț
Produs
Total produse
Vezi coșul
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 de Serge Autexier

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

Observăm în volumul Intelligent Computer Mathematics o abordare interdisciplinară riguroasă, care forțează granițele tradiționale dintre inteligența artificială, calculul simbolic și managementul informației. Lucrarea nu se limitează la o singură sferă de cercetare, ci explorează modul în care tehnicile de IA pot fi integrate în rezolvarea problemelor matematice complexe și, invers, cum calculul simbolic poate sprijini dezvoltarea algoritmilor de învățare automată. Această ediție din 2010, editată de Serge Autexier și colegii săi, extinde cadrul propus de Integrating Symbolic Mathematical Computation and Artificial Intelligence cu date noi din perioada 2007-2010, punând un accent deosebit pe sistemele de asistență matematică mecanizată.

Suntem de părere că structura volumului reflectă o progresie logică de la fundamentul teoretic la aplicații practice. Prima secțiune, dedicată AISC, analizează provocările funcțiilor multivalente și modelele matematice de imunitate dobândită. Urmează contribuțiile Calculemus, care se concentrează pe uzabilitatea demonstratoarelor interactive de teoreme și pe descompunerea domeniilor simbolice. În final, secțiunea MKM abordează managementul cunoștințelor, o nișă aflată la intersecția matematicii cu biblioteconomia și publicarea științifică. Această organizare tripartită demonstrează o maturizare a domeniului față de lucrările anterioare, precum Towards Mechanized Mathematical Assistants, prin includerea unor studii de caz concrete despre dezvoltarea formală structurată în Isabelle/HOL sau interpretările matriciale peste numere raționale. Stilul este pur academic, specific seriei Lecture Notes in Computer Science, fiind orientat către precizie tehnică și prezentarea sistemelor care vor deveni instrumente de lucru cotidiene pentru ingineri și matematicieni.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 38599 lei

Puncte Express: 579

Carte disponibilă

Livrare economică 30 aprilie-14 mai

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă

Specificații

ISBN-13: 9783642141270
ISBN-10: 3642141277
Pagini: 486
Ilustrații: XV, 471 p. 71 illus.
Dimensiuni: 10 x 93 x 33 mm
Greutate: 0.73 kg
Ediția:2010
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ă

Research

De ce să citești această carte

Recomandăm această lucrare cercetătorilor care doresc să înțeleagă convergența dintre inteligența artificială și calculul simbolic. Cititorul câștigă o perspectivă de ansamblu asupra celor mai recente metode de management al cunoștințelor matematice și automatizarea deducției. Este un volum esențial pentru cei care lucrează la dezvoltarea demonstratoarelor de teoreme sau a sistemelor de asistență matematică, oferind soluții concrete pentru combaterea fragmentării în comunitatea științifică.

Cuprins

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 ofFormality: 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.

Descriere

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."