Intelligent computer mathematics, 11 conf., CICM 2018

Preface......Page 6
Organization......Page 9
Contents......Page 11
 1 Introduction......Page 13
 3 Description of the New Technology......Page 14
  3.5 transitive.xsl......Page 15
  3.9 Remote Service and Processing Times......Page 16
 References......Page 17
 1 Introduction......Page 19
  2.1 Preliminaries: LUTINS......Page 21
  2.2 Preliminaries: IMPS......Page 23
  2.3 Preliminaries: OMDoc/MMT......Page 25
  3.1 The LUTINS Theory in LF......Page 26
  3.2 Translation......Page 27
 4 Applications......Page 31
 5 Conclusion......Page 32
 References......Page 33
 1 Introduction......Page 35
 2 Background: The Isabelle System......Page 36
 3 Isabelle/DOF......Page 38
  4.1 The Scholar Paper Scenario: Eating One's Own Dog Food......Page 39
  4.2 The Math-Exam Scenario......Page 42
  4.3 The Certification Scenario Following CENELEC......Page 45
  5.1 A Scholarly Paper......Page 46
  5.2 CENELEC......Page 47
 6 Conclusion and Related Work......Page 48
 References......Page 50
 1 Problem and Current State......Page 51
  2.1 First Extraction Scan......Page 53
  2.3 Ongoing Semantic Enhancement for Second Extraction Scan......Page 55
 3 CAS Verification Procedure for DLMF Formulae......Page 57
  3.2 Constraint Handling......Page 58
 4 Summary......Page 60
 References......Page 63
 1 Introduction......Page 65
 3 Coq and Coq Automation......Page 66
 4 Case Studies......Page 67
 5 Conclusion......Page 70
 References......Page 71
 1 Introduction......Page 72
  2.1 Orthoptics of Conics......Page 73
  2.2 Generalization to Other Curves......Page 75
 3 The First Approach......Page 77
 4 The Second Approach......Page 82
  4.1 Implementation Issues......Page 83
  4.2 Isoptics......Page 84
 5 Conclusion......Page 86
 References......Page 87
 1 Motivation......Page 88
 2 Background Ideas......Page 90
 3 Project Objectives......Page 92
 4 Work Plan Status......Page 93
 6 Conclusion......Page 95
 References......Page 96
 1 Introduction......Page 99
  2.1 Signals and Operations......Page 100
  2.2 Linear Time Invariant Filters......Page 101
  2.4 Constant-Coefficient Difference Equation......Page 102
  3.1 Signals and Filters......Page 103
  3.2 Recursion over Z......Page 104
  4.1 Direct Form I......Page 105
  4.3 State-Space......Page 107
  5.1 Error Filter......Page 110
  5.2 Worst-Case Peak Gain Theorem......Page 111
 6 Conclusions and Perspectives......Page 113
 References......Page 114
 1 Introduction......Page 116
 2 Related Work......Page 117
 3 MathTools......Page 118
 4 Conclusion and Future Work......Page 120
 References......Page 121
 1 Introduction......Page 123
 2 Background and Notation......Page 124
 3 System Description of Aligator.jl......Page 125
 4 Experimental Evaluation......Page 127
 References......Page 128
 1 ENIGMA: Efficient Learning of Given Clause Guidance......Page 130
 2 Enhanced ENIGMA Features and Classifiers......Page 131
 3 Experimental Evaluation......Page 133
 References......Page 135
 1 Introduction......Page 137
  2.1 Conditions......Page 138
  2.4 Theorems......Page 139
  2.6 Spaces, Structures and Models......Page 140
 3 Conclusions......Page 141
 References......Page 142
 1 Introduction......Page 143
 2 Existing Mizar Exports......Page 144
 4 Isabelle Import Infrastructure......Page 147
 5 Mizar-Style Proof Development in Isabelle......Page 149
  6.1 Procedure Overview......Page 151
  6.2 Background Information......Page 152
  6.3 Definitions......Page 153
  6.4 Redefinitions......Page 154
 7 Conclusion......Page 156
 References......Page 157
 1 Introduction......Page 159
 2 The Eye-Tracking Study......Page 161
 3 Patterns in the Gaze Plots......Page 162
 4 Patterns in the Elicited Data......Page 166
  4.1 Structure-Driven Areas of Interest......Page 167
  4.2 Math-Driven Areas of Interest......Page 169
  4.3 What are Cognitive Units (Words) in Math?......Page 170
 5 A Nascent Theory for Mathematical Documents......Page 171
  5.1 Design Application: Interactive Documents......Page 172
 6 Conclusion......Page 173
 References......Page 174
 1 Introduction......Page 176
  2.1 Constructibility......Page 177
  2.2 An Algebraic Formula for the Vertices......Page 178
 3 Example Statements......Page 180
  3.1 Lengths in a Regular Pentagon......Page 181
  3.2 Lengths in a Regular 11-gon......Page 185
  3.3 Implementation in GeoGebra......Page 186
 References......Page 188
 1 Introduction......Page 190
  1.1 Related Work......Page 191
  2.1 Power-Products......Page 192
  2.2 Polynomials......Page 193
 3 Gröbner Bases and Buchberger's Algorithm......Page 195
  3.2 Gröbner Bases......Page 196
  3.3 An Algorithm Schema for Computing Gröbner Bases......Page 197
  3.4 Buchberger's Algorithm......Page 198
 4 Faugère's F4 Algorithm......Page 199
  5.1 Reduced Gröbner Bases......Page 201
  5.2 Gröbner Bases of Syzygy Modules......Page 202
 6 Conclusion......Page 203
 References......Page 204
 1 Introduction......Page 206
 2 Technical Background Information......Page 207
  3.1 Example of Collaborative Algorithm Discovery......Page 208
  3.3 Collaborative Computation Model (CCM)......Page 209
  3.4 Formalized Hypothesis on Algorithm Discovery......Page 211
 4 Formally Describing Learned Algorithmic Knowledge......Page 212
  5.1 MathChat Features for Realizing the Social Machines......Page 213
  5.2 Application in Online Education and Pilot Investigation......Page 214
 6 Discussion, Limitations and Future Directions......Page 216
 References......Page 219
 1 Introduction......Page 221
 2 Preliminaries: MMT and Views......Page 223
 3 Intra-Library View Finding......Page 224
  3.1 Preprocessing......Page 225
  3.2 Search......Page 227
  3.3 Optimizations......Page 228
 4 Inter-Library View Finding......Page 230
  4.1 The PVS/NASA Library......Page 231
  4.2 Implementation......Page 232
 5 Conclusion......Page 233
 References......Page 235
 1 Introduction......Page 237
  2.1 Identifying Valuable Conjectures via Proof Search......Page 238
  2.2 Conjecturing......Page 239
 References......Page 242
 1 Introduction and Motivation......Page 244
  2.1 The MaMoReD Approach......Page 246
  2.3 Theory Graphs......Page 247
  2.4 MoSIS: Creating ExaSlang Layer 0......Page 248
  3.1 A Theory Graph for PDE Knowledge......Page 249
  3.2 Automating Model Knowledge Amalgamation......Page 252
  3.3 Implementation: Realizing MoSIS via Jupyter and Mmt......Page 254
 4 Conclusion and Future Work......Page 257
 References......Page 258
 1 Introduction......Page 260
 2 Checking Theorems and Algorithms......Page 261
 References......Page 265
 1 Introduction: Autoformalization......Page 267
 2 Neural Translation......Page 268
  2.2 RNN and the RNN Memory Cell......Page 269
  2.3 Attention Mechanism......Page 270
 3 The Informalized Dataset......Page 272
  4.1 Data Preprocessing......Page 273
  4.3 Choosing Hyperparameters......Page 274
  5.1 Choosing the Best Memory Cell and Attention Mechanism......Page 275
  5.2 The Effect of Optimizers, Residuals and Encodings with Respect to Layers......Page 276
  5.4 Greedy Covers and Edit Distances......Page 277
  5.5 Translating from Mizar to LaTeX......Page 278
 6 A Translation Example......Page 279
 7 Conclusion and Future Work......Page 280
 References......Page 281
 1 Introduction......Page 283
 2 Objectives of the Project......Page 285
 4 Foundations and Related Work......Page 286
  4.1 The Parts-of-Math Tagger......Page 287
  4.2 Lcolor push gray 0color popTto10AT.4exExml......Page 288
 5 The Datasets to Be Collected, Created and Used......Page 289
 6 Samples of Tagging and Disambiguation Algorithms......Page 290
  6.2 Disambiguation......Page 291
 7 DNN's for Math Sequence-to-Sequence Translation......Page 293
 8 Testing and Performance Evaluation......Page 294
 9 Stages of the Project......Page 295
 References......Page 296
Author Index......Page 299