دانلود کتاب Intelligent Computer Mathematics: 10 conf., AISC2010, 17 conf., Calculemus 2010, 9 conf., MKM2010

عنوان فارسی :

دانلود کتاب ریاضیات رایانه ای رایانه ای: 10 کنفرانس ، AISC2010 ، 17 کنفرانس ، حسابگر 2010 ، 9 کنف ، MKM2010

عنوان انگلیسی :

Intelligent Computer Mathematics: 10 conf., AISC2010, 17 conf., Calculemus 2010, 9 conf., MKM2010

زبان : English

موضوع : Mathematics

نویسندگان : Serge Autexier Jacques Calmet David Delahaye P.D.F. Ion Laurence Rideau Renaud Rioboo Alan P. Sexton

ناشر : Springer

ISBN (شابک) : 3642141277, 9783642141270

تعداد صفحات : 485\485

سال نشر : 2010     ویرایش : 1st Edition.

حجم : 5 MB       فرمت : pdf

قیمت : 20000 تومان

فهرست :



Table of contents :
Cover......Page 1
Title......Page 3
Copyright......Page 4
Preface......Page 5
AISC, Calculemus and MKM Organization......Page 7
Table of Contents......Page 13
Introduction......Page 16
The (Bourbakist) Theory......Page 17
The Branch View......Page 18
The Table-Maker's Point of View......Page 19
Differential Algebra......Page 20
A Different Point of View......Page 21
The (Bourbakist) Theory......Page 22
The Multivalued View......Page 23
The Table-Maker's Point of View......Page 24
Conclusion......Page 25
References......Page 26
The Dynamic Dictionary of Mathematical Functions......Page 28
The Picture in 1997......Page 29
Hits......Page 30
Misses......Page 31
Suggestions for the Future......Page 32
References......Page 33
{\it I }-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness......Page 34
Positions and Subterms......Page 36
I-Term Ordering......Page 38
Clauses, Redundancy Criteria and Selection Functions......Page 39
Non Equational Case......Page 40
Equational Case......Page 41
References......Page 47
Introduction......Page 49
Isabelle and Theory Morphisms......Page 50
The Theory QuotientType-Param......Page 51
Defining Functions over Quotient Types......Page 52
The Theory Fold-Param......Page 54
The Theory Fold......Page 55
Specifying Finite Sets and Bags......Page 56
Implementing Bags......Page 57
Implementing Finite Sets......Page 59
Conclusions......Page 62
References......Page 63
Introduction......Page 64
Preliminaries......Page 66
$Z$-Clauses......Page 67
Instantiation of Inequality Formulas......Page 69
Properties of Inferences on $Z$-Clauses......Page 70
Completeness of the Combined Instantiation Schemes......Page 72
Applications......Page 73
Discussion......Page 77
References......Page 78
Generating Function......Page 79
Canonical Appell System......Page 80
Krawtchouk Expansions......Page 81
Krawtchouk Polynomials in Coding Theory......Page 82
Inverse Transform......Page 83
Symmetric Representation of a Matrix......Page 85
General Construction of Orthogonal Polynomials with Respect to a Multinomial Distribution......Page 87
Examples......Page 88
References......Page 89
Introduction......Page 91
Mathematical Model......Page 95
Approximate Solution of the Model......Page 98
Numerical Experiments and Discussion......Page 99
References......Page 101
Introduction......Page 104
Preliminaries......Page 107
Main Results......Page 108
Preliminaries......Page 111
Main Results......Page 112
References......Page 115
Introduction......Page 116
Syntax......Page 117
Semantics......Page 118
$\alpha-\beta$ Pruning......Page 123
Tropical Games......Page 124
Soundness of Tropical Pruning......Page 125
Parsing as a Tropical Game......Page 127
References......Page 130
Introduction......Page 131
Numbers as Matrices......Page 133
Transforming Matrices of Numbers......Page 134
Representing Integer Numbers as Matrices......Page 135
Use of Nilpotent Matrices......Page 136
Matrix Interpretations Revisited......Page 138
Testing Universally Quantified Symbolic Constraints......Page 140
Solving Existentially Quantified Arithmetic Constraints......Page 141
Conclusions......Page 144
References......Page 145
Introduction and Motivation......Page 147
SystemOnTPTP......Page 148
MizAR......Page 149
Server-Based Verification of a Mizar Article......Page 150
HTMLization of Mizar Articles......Page 152
Generation of ATP Problems in TPTP Format......Page 153
Calling ATP Systems......Page 154
Getting Hints for Necessary Mizar References......Page 157
Future Work and Conclusions......Page 158
References......Page 159
Introduction......Page 162
The Structure of (Procedural) Formal Developments......Page 164
Small and Large Scale Automation......Page 166
Local and Global Knowledge......Page 167
Exploiting the Library......Page 169
References......Page 170
Mechanized Mathematics......Page 172
Introduction......Page 173
The Frama-C Software......Page 174
Combinatorial and Algebraic Background: Integer Partitions......Page 175
Properties......Page 177
SCHUR Implementation......Page 178
Annotations......Page 179
Proofs......Page 181
Problems, Mistakes......Page 183
Conclusion and Future Work......Page 185
References......Page 186
Introduction......Page 187
Partitions and Piecewise Functions......Page 189
Hybrid Sets......Page 190
Functions of Hybrid Domain......Page 192
Generalised Partitions......Page 193
Refinement......Page 194
Pseudo-functions and Pseudo-relations......Page 195
Hybrid Domain Decomposition......Page 196
Arithmetic on Piecewise Functions......Page 197
Identities for Invertible Operators......Page 198
Matrix Addition......Page 199
Symbolic Spline Interpolation......Page 201
Conclusion......Page 202
References......Page 203
Introduction......Page 204
Preliminaries......Page 205
Formalization Issues......Page 206
Quantifier Elimination by Projection......Page 208
Decidability......Page 210
Pseudo-divisions, Pseudo-gcd......Page 211
Common Roots, Exclusive Roots......Page 212
Quantifier Elimination for Algebraically Closed Fields......Page 214
Conclusion......Page 216
References......Page 217
Introduction......Page 219
Algebraic Data Structures in Coq......Page 221
Effective Homology of the Cone in Coq......Page 224
Instances of Chain Complexes of Infinite Type......Page 226
Computing with Infinite Data Structures in Coq......Page 228
Conclusions and Further Work......Page 231
References......Page 232
Interval Analysis and Validation......Page 234
Definitions......Page 235
Operations on Intervals......Page 238
More Results on Real Matrices......Page 240
Interval Matrices......Page 241
The Solution Set of a System of Linear Interval Equations......Page 242
Basic Regularity Criteria......Page 243
Verifiable Regularity Criteria......Page 244
Conclusion......Page 246
References......Page 247
Introduction......Page 249
Basic Details of System......Page 250
Performance Comparison with Other Systems......Page 251
First Case Study: Alternative Strategies......Page 252
Remarks......Page 254
Preliminary Strategy 1......Page 255
An Optimal Strategy......Page 256
Second Case Study: Two-Part Reduction......Page 257
References......Page 260
Introduction......Page 262
Computing in Bijective Base-2......Page 263
Sharing Axiomatizations with Type Classes......Page 264
The 5 Primitive Operations......Page 265
Peano Arithmetic......Page 266
Computing with {\ it Hereditarily Finite Sets}......Page 267
Arithmetic Operations......Page 269
Adding Other Arithmetic Operations......Page 271
Deriving Set Operations......Page 272
Deriving an Instance with Fast Bitstring Operations......Page 274
Related Work......Page 275
References......Page 276
Against Rigor......Page 277
Introduction......Page 278
The Matita Superposition Tool......Page 279
The Main Algorithm......Page 280
Performance Issues......Page 282
Interfacing CIC and the Superposition Engine......Page 283
(Re)construction of the Proof Term......Page 285
Smart Application......Page 286
Examples......Page 287
Related Works and Systems......Page 289
Conclusions......Page 290
References......Page 291
Motivation......Page 293
Originality......Page 295
Architecture and Communication......Page 296
Design of Geometric Textbook Knowledge Base......Page 297
Knowledge Representation......Page 299
Creation of the Geometric Textbook Knowledge Base......Page 300
User Interface of Electronic Geometry Textbook......Page 302
Presentation of Geometric Textbook Knowledge......Page 304
Conclusion and Future Work......Page 305
References......Page 306
Introduction......Page 308
Coordinate Frames......Page 309
Vectors and Covectors......Page 311
Higher Order Tensors......Page 313
References......Page 314
Introduction......Page 315
Different Proofs of a Theorem......Page 316
Different Mathematical Versions......Page 318
Different Technical Versions......Page 319
Abstract and Concrete Mathematics......Page 320
Representational Issues......Page 322
Generalization of Theorems......Page 323
Which Way To Go?......Page 324
MML — The State of the Art......Page 326
Conclusions......Page 327
References......Page 328
Introduction......Page 330
Customization from Four Perspectives......Page 332
Case Study: Controlling the Solutions for an Exercise......Page 333
Case Study: Creating New Exercises from Existing Parts......Page 334
Rewrite Rules......Page 335
Views and Canonical Forms......Page 336
Exercises......Page 337
Representing Rewrite Rules......Page 338
Representing Rewrite Strategies......Page 339
Configuring Rewrite Strategies......Page 341
Case Studies Revisited......Page 342
Conclusions, Related and Future Work......Page 343
References......Page 344
Different Questions, Different Sources......Page 346
General View of the System......Page 347
Putting All Together......Page 348
References......Page 349
Introduction......Page 351
$_S$T$_E$X: Object-Oriented L$^A$T$_E$X Markup......Page 352
User Interface Features of $_S$T$_E$X IDE......Page 354
Implementation......Page 356
References......Page 358
Introduction......Page 360
The Logician's View......Page 361
The Mathematician's View......Page 362
The Deductionist's View......Page 363
How to Make Systems More Accepted?......Page 365
References......Page 368
Introduction......Page 370
Dimensions of Formality in SAMSDocs......Page 371
Multi-dimensional Information Needs......Page 375
Multi-dimensional Markup......Page 376
Multi-dimensional Services with MKM Technology......Page 378
Conclusion and Further Work......Page 380
References......Page 382
Introduction......Page 385
A Scalable Representation Language......Page 386
Module System......Page 387
Foundation-Independence......Page 389
Symbol Identifiers ``in the Large''......Page 390
Validation......Page 392
Querying......Page 393
Presentation......Page 394
Generating Content......Page 395
Retrieving Content......Page 396
Conclusion and Future Work......Page 397
References......Page 398
Introduction......Page 400
Challenges of Content MathML Support......Page 401
Overview of the Formulator MathML Editor......Page 402
General Approach to the Document Structure......Page 404
Improving Usability for a Template-Based Approach......Page 406
Examples of Free-Style Editing......Page 407
Supporting Users Accustomed to Legacy Input......Page 409
Availability and Future Work......Page 410
References......Page 411
Introduction......Page 413
Related Works......Page 414
Notational Diversity Accross Cultures......Page 415
Difference Because of Names Differences......Page 416
Same Notations, Different Concepts......Page 417
The Notation Census......Page 418
Ingredients......Page 419
Evolution......Page 420
Notations for ActiveMath......Page 422
Conclusion......Page 423
References......Page 424
Introduction......Page 426
Pre-EA Stage (1962–1970)......Page 428
EA and Russian SAD (1971 - 1992)......Page 429
Theoretical Work......Page 430
Experimental Work......Page 432
Team Evolution (or the Sad Part of the SAD History)......Page 433
Post-EA Stage and English SAD (1998-Nowadays)......Page 434
Conclusion......Page 435
References......Page 436
Introduction......Page 442
Stability of Networks......Page 443
The Mizar System......Page 446
Preliminaries about Rational Functions......Page 447
The Theorem......Page 448
Discussion — Lessons Learned......Page 450
Representation of Knowledge......Page 451
Conclusions......Page 452
References......Page 453
Introduction......Page 455
Background and Use Cases......Page 457
The Proof Movie......Page 459
The Proviola: Watching a Proof Movie......Page 460
The Camera: Creating a Proof Movie......Page 462
Proxying Movie-Making......Page 463
The Camera as a Service Broker......Page 465
Towards an Encyclopedia of Formal Proof......Page 466
Related Work......Page 467
References......Page 468
Introduction and Motivation......Page 470
Use Cases......Page 472
Towards Distributed Collaboration......Page 473
A Special Case: The Mizar Developers......Page 474
Formal Wiki Features and Issues......Page 476
Degrees of Formal Correctness and Coherence......Page 477
Prototype......Page 478
Prototype Implementation......Page 480
References......Page 483
Author Index......Page 485





کتاب های پزشکی

دانلود کتاب Essentials of Family Medicine

دانلود کتاب Basic clinical neuroscience

دانلود کتاب Advanced Medicine Recall

دانلود کتاب The Encyclopedia of Arthritis (Facts on File Library of Health and Living)

دانلود کتاب Atlas of Normal Roentgen Variants That May Simulate Disease

کتاب های کامپیوتر

دانلود کتاب .NET Windows Forms in 21 Tagen . Oberflächen programmieren

دانلود کتاب Functional Programming for Java Developers

دانلود کتاب

دانلود کتاب IMAGE SEGMENTATION

دانلود کتاب Artificial intelligence and soft computing

کتاب های ریاضی

دانلود کتاب Global analysis of minimal surfaces

دانلود کتاب Dynamical systems with applications using Maple

دانلود کتاب Control theory of systems governed by partial differential equations

دانلود کتاب Analytic number theory

دانلود کتاب Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Vol. 1

کتاب های تکنولوژی

دانلود کتاب Formability of Metallic Materials: Plastic Anisotropy, Formability Testing, Forming Limits

دانلود کتاب NanoBiotechnology Protocols

دانلود کتاب Quality Standard for Steel Castings for Valves, Flanges, Fittings, and Other Piping Components: Visual Method (Sp-55)

دانلود کتاب Hybrid Nanomaterials: Synthesis, Characterization, and Applications

دانلود کتاب Protein Analysis and Purification

کتاب های مذهبی

دانلود کتاب

دانلود کتاب Djinn Summoning

دانلود کتاب Systematic Theology: An Introduction to Biblical Doctrine

دانلود کتاب Alchemy & Mysticism

دانلود کتاب Zwingli and Bullinger (Library of Christian Classics)

کتاب های فیزیولوژی

دانلود کتاب Culture in Mind - Cognition, Culture, and the Problem of Meaning

دانلود کتاب The Psychology of Eating: From Healthy to Disordered Behavior

دانلود کتاب Psychology: From Inquiry to Understanding (2nd Edition)

دانلود کتاب Carnal Comics Brittany Andrews

دانلود کتاب Practical Teaching Skills for Driving Instructors

کتاب های تاریخی

دانلود کتاب War, State, and Society in England and the Netherlands 1477-1559

دانلود کتاب The Official Monogram Us Navy & Marine Corps Aircraft Color Guide: 1960-1993

دانلود کتاب The Royal Navy: A History From The Earliest Times To 1900 Vol.V

دانلود کتاب Tupolev Tu-95/-142 (Russian Aircraft in Action)

دانلود کتاب Republic P-47 Thunderbolt

کتاب های زیست شناسی

دانلود کتاب The Essential Psychedelic Guide

دانلود کتاب Special Issue: Age and Growth of Chondrichthyan Fishes: New Methods, Techniques and Analysis (Developments in Environmental Biology of Fishes)

دانلود کتاب The Future of Visual Anthropology: Engaging the Senses

دانلود کتاب Handbook of Statistical Systems Biology

دانلود کتاب Hormones and Reproduction of Vertebrates - Volume 5: Mammals

کتاب های اقتصاد

دانلود کتاب Enterprise Resource Planning Solutions and Management

دانلود کتاب Marketing Management: A Relationship Approach

دانلود کتاب European Collaboration in Research and Development: Business Strategy and Public Policy

دانلود کتاب Virtualization with Xen (tm): Including XenEnterprise, XenServer, and XenExpress

دانلود کتاب Making Enterprise Risk Management Pay Off: How Leading Companies Implement Risk Management

کتاب های آموزشی

دانلود کتاب Logics in Artificial Intelligence: 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004. Proceedings

دانلود کتاب AsiaSim 2007: Asia Simulation Conference 2007, Seoul, Korea, October 10-12, 2007, Proceedings (Communications in Computer and Information Science)

دانلود کتاب How to Do Everything with Microsoft Office Excel 2003 (How to Do Everything)

دانلود کتاب Aptitude for Destruction, Volume 2: Case Studies of Organizational Learning in Five Terrorist Groups

دانلود کتاب The Gale Encyclopedia of the Unusual and Unexplained

کتاب های حقوق

دانلود کتاب Last Words and the Death Penalty: Voices of the Condemned and Their Co-victims (Criminal Justice: Recent Scholarship)

دانلود کتاب Facing the Limits of the Law

دانلود کتاب The Tax Law of Unrelated Business for Nonprofit Organizations

دانلود کتاب Max Planck Yearbook of United Nations Law, Volume 11 (2007)

دانلود کتاب Law: A Very Short Introduction (Very Short Introductions)

کتاب های علوم انسانی

دانلود کتاب Riddles Of Existence: A Guided Tour Of Metaphysics

دانلود کتاب The Work of the American Meteor Society in 1914 and 1915

دانلود کتاب Philosophy: History, Ideas, Theories, Who's Who, How to Think

دانلود کتاب Plato’s Progress

دانلود کتاب An Examination of Sir William Hamilton's Philosophy: And of the Principal Philosophical Questions Discussed in His Writings