000 04961nam a22005775i 4500
001 978-3-642-14128-7
003 DE-He213
005 20240730192259.0
007 cr nn 008mamaa
008 100629s2010 gw | s |||| 0|eng d
020 _a9783642141287
_9978-3-642-14128-7
024 7 _a10.1007/978-3-642-14128-7
_2doi
050 4 _aQA150-272
072 7 _aPBF
_2bicssc
072 7 _aMAT002000
_2bisacsh
072 7 _aPBF
_2thema
082 0 4 _a512
_223
245 1 0 _aIntelligent Computer Mathematics
_h[electronic resource] :
_b10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings /
_cedited by Serge Autexier, Jacques Calmet, David Delahaye, P.D.F. Ion, Laurence Rideau, Renaud Rioboo, Alan Sexton.
250 _a1st ed. 2010.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2010.
300 _aXV, 471 p. 71 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v6167
505 0 _aContributions 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.
650 0 _aAlgebra.
_921222
650 0 _aArtificial intelligence.
_93407
650 1 4 _aAlgebra.
_921222
650 2 4 _aArtificial Intelligence.
_93407
700 1 _aAutexier, Serge.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149343
700 1 _aCalmet, Jacques.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149344
700 1 _aDelahaye, David.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149345
700 1 _aIon, P.D.F.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149346
700 1 _aRideau, Laurence.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149347
700 1 _aRioboo, Renaud.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149348
700 1 _aSexton, Alan.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9149349
710 2 _aSpringerLink (Online service)
_9149350
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783642141270
776 0 8 _iPrinted edition:
_z9783642141294
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v6167
_9149351
856 4 0 _uhttps://doi.org/10.1007/978-3-642-14128-7
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c94170
_d94170