This book constitutes the joint refereed proceedings of the 10th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2010, the 17th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2010, and the 9th International Conference on Mathematical Knowledge Management, MKM 2010. All submissions passed through a rigorous review process. From the 25 papers submitted to AISC 2010, 9 were selected for presentation at the conference and inclusion in the proceedings volume. A total of 14 papers were submitted to Calculemus, of which 7 were accepted. MKM 2010 received 27 submissions, of which 16 were accepted for presentation and publication. The events focused on the use of AI techniques within symbolic computation and the application of symbolic computation to AI problem solving; the combination of computer algebra systems and automated deduction systems; and mathematical knowledge management, respectively.
Author(s): Serge Autexier, Jacques Calmet, David Delahaye, P.D.F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton
Series: Lecture notes in Artificial Intelligence 6167
Edition: 1st Edition.
Publisher: Springer
Year: 2010
Language: English
Pages: 485
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
