Abstract is missing.
- What International Studies Say about the Importance and Limitations of Using Computers to Teach Mathematics in Secondary SchoolsJaime Carvalho e Silva. 1-11 [doi]
- Towards Robust Hyperlinks for Web-Based Scholarly CommunicationHerbert Van de Sompel, Martin Klein, Harihar Shankar. 12-25 [doi]
- Computable Data, Mathematics, and Digital Libraries in Mathematica and Wolfram|AlphaEric W. Weisstein. 26-29 [doi]
- Towards the Formal Reliability Analysis of Oil and Gas PipelinesWaqar Ahmed, Osman Hasan, Sofiène Tahar, Mohammad Salah Hamdi. 30-44 [doi]
- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular DecompositionMatthew England, Russell J. Bradford, Changbo Chen, James H. Davenport, Marc Moreno Maza, David J. Wilson. 45-60 [doi]
- A Tableaux-Based Decision Procedure for Multi-parameter Propositional SchemataDavid Cerna. 61-75 [doi]
- Detecting Unknots via Equational Reasoning, I: ExplorationAndrew Fish, Alexei Lisitsa. 76-91 [doi]
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic DecompositionZongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge. 92-107 [doi]
- Hipster: Integrating Theory Exploration in a Proof AssistantMoa Johansson, Dan Rosén, Nicholas Smallbone, Koen Claessen. 108-122 [doi]
- Formalization of Complex Vectors in Higher-Order LogicSanaz Khan Afshar, Vincent Aravantinos, Osman Hasan, Sofiène Tahar. 123-137 [doi]
- A Mathematical Structure for Modeling InventionsBernd Wegner, Sigram Schindler. 138-152 [doi]
- Search Interfaces for MathematiciansAndrea Kohlhase. 153-168 [doi]
- A Data Model and Encoding for a Semantic, Multilingual Terminology of MathematicsMichael Kohlhase. 169-183 [doi]
- PDF/A-3u as an Archival Format for Accessible MathematicsRoss Moore. 184-199 [doi]
- Which One Is Better: Presentation-Based or Content-Based Math Search?Minh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topic, Akiko Aizawa. 200-212 [doi]
- POS Tagging and Its Applications for Mathematics - Text Analysis in MathematicsUlf Schöneberg, Wolfram Sperber. 213-223 [doi]
- Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for WikipediaMoritz Schubotz, Gabriel Wicke. 224-235 [doi]
- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?Marco B. Caminati, Manfred Kerber, Christoph Lange 0002, Colin Rowat. 236-251 [doi]
- Realms: A Structure for Consolidating Knowledge about Mathematical TheoriesJacques Carette, William M. Farmer, Michael Kohlhase. 252-266 [doi]
- Matching Concepts across HOL LibrariesThibault Gauthier, Cezary Kaliszyk. 267-281 [doi]
- Mining State-Based Models from Proof CorporaThomas Gransden, Neil Walkinshaw, Rajeev Raman. 282-297 [doi]
- Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency LatticesYannis Haralambous, Pedro Quaresma. 298-311 [doi]
- Flexary Operators for Formalized MathematicsFulya Horozal, Florian Rabe, Michael Kohlhase. 312-327 [doi]
- Interactive Simplifier Tracing and Debugging in IsabelleLars Hupel. 328-343 [doi]
- Towards an Interaction-based Integration of MKM Services into End-User ApplicationsConstantin Jucovschi. 344-356 [doi]
- Towards Knowledge Management for HOL LightCezary Kaliszyk, Florian Rabe. 357-372 [doi]
- Automated Improving of Proof Legibility in the Mizar SystemKarol Pak. 373-387 [doi]
- A Vernacular for Coherent LogicSana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic. 388-403 [doi]
- An Approach to Math-Similarity SearchQun Zhang, Abdou Youssef. 404-418 [doi]
- Digital Repository of Mathematical FormulaeHoward S. Cohl, Marjorie A. McClain, Bonita V. Saunders, Moritz Schubotz, Janelle C. Williams. 419-422 [doi]
- NNexus ReloadedDeyan Ginev, Joseph Corneli. 423-426 [doi]
- E-books and Graphics withDeyan Ginev, Bruce R. Miller, Silviu Oprea. 427-430 [doi]
- System Description: MathHub.infoMihnea Iancu, Constantin Jucovschi, Michael Kohlhase, Tom Wiesing. 431-434 [doi]
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project DescriptionCezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers. 435-439 [doi]
- System Description: A Semantics-Aware LaTeX-to-Office ConverterLukas Kohlhase, Michael Kohlhase. 440-443 [doi]
- Math Indexer and Searcher Web Interface - Towards Fulfillment of Mathematicians' Information NeedsMartin Líska, Petr Sojka, Michal Ruzicka. 444-448 [doi]
- SAT-Enhanced Mizar Proof CheckingAdam Naumowicz. 449-452 [doi]
- A Framework for Formal Reasoning about Geometrical OpticsUmair Siddique, Sofiène Tahar. 453-456 [doi]