Abstract is missing.
- DeepAlgebra - An Outline of a ProgramPrzemyslaw Chojecki. 1-8 [doi]
- Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case StudyJacques Carette, William M. Farmer. 9-24 [doi]
- The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and TheoremaAlexander Maletzky, Wolfgang Windsteiger. 25-39 [doi]
- Automatically Proving Equivalence by Type-Safe ReflectionFranck Slama, Edwin Brady. 40-55 [doi]
- The Global Digital Mathematics Library and the International Mathematical Knowledge TrustPatrick D. F. Ion, Stephen M. Watt. 56-69 [doi]
- The New Numdam PlatformThierry Bouche, Olivier Labbe. 70-82 [doi]
- Classification of Alignments Between Concepts of Formal Mathematical SystemsDennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe. 83-98 [doi]
- Software Citations, Information Systems, and BeyondMichael Kohlhase, Wolfram Sperber. 99-114 [doi]
- Semantic Preserving Bijective Mappings of Mathematical Formulae Between Document Preparation Systems and Computer Algebra SystemsHoward S. Cohl, Moritz Schubotz, Abdou Youssef, André Greiner-Petter, Jürgen Gerhard, Bonita V. Saunders, Marjorie A. McClain, Joon Bang, Kevin Chen. 115-131 [doi]
- Towards Mathematical AI via a Model of the Content and Process of Mathematical Question and Answer DialoguesJoseph Corneli, Ursula Martin, Dave Murray-Rust, Alison Pease. 132-146 [doi]
- Theory Morphisms in Church's Type Theory with Quotation and EvaluationWilliam M. Farmer. 147-162 [doi]
- Semantic Representation of General Topology in the Wolfram LanguageIan Ford. 163-177 [doi]
- Zeta Types and Tannakian Symbols as a Method for Representing Mathematical KnowledgeAndreas Holmstrom, Torstein Vik. 178-192 [doi]
- Presentation and Manipulation of Mizar Properties in an Isabelle Object LogicCezary Kaliszyk, Karol Pak. 193-207 [doi]
- Visual Structure in Mathematical ExpressionsAndrea Kohlhase, Michael Kohlhase, Michael Fürsich. 208-223 [doi]
- Mathematical Models as Research Data via Flexiformal Theory GraphsMichael Kohlhase, Thomas Koprucki, Dennis Müller, Karsten Tabelow. 224-238 [doi]
- A Verified Algorithm Enumerating Event StructuresJuliana Bowles, Marco B. Caminati. 239-254 [doi]
- Reasoning with Concept Diagrams About Antipatterns in OntologiesZohreh Shams, Mateja Jamnik, Gem Stapleton, Yuri Sato. 255-271 [doi]
- A Web-Based Toolkit for Mathematical Word Processing Applications with SemanticsNathan C. Carter, Kenneth G. Monks. 272-291 [doi]
- ENIGMA: Efficient Learning-Based Inference Guiding MachineJan Jakubuv, Josef Urban. 292-302 [doi]
- Proof Mining with Dependent TypesEkaterina Komendantskaya, Jónathan Heras. 303-318 [doi]
- Formalization of Transform Methods Using HOL LightAdnan Rashid, Osman Hasan. 319-332 [doi]
- Combining Refinement and Signal-Temporal Logic for Biological SystemsUsman Sanwal, Umair Siddique. 333-339 [doi]
- VMEXT: A Visualization Tool for Mathematical Expression TreesMoritz Schubotz, Norman Meuschke, Thomas Hepp, Howard S. Cohl, Bela Gipp. 340-355 [doi]
- Part-of-Math Tagging and ApplicationsAbdou Youssef. 356-374 [doi]