Abstract is missing.
- Mathematical Theory Exploration in Theorema: Reduction RingsAlexander Maletzky. 3-17 [doi]
- Formalization of Bing's Shrinking Method in Geometric TopologyKen'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto. 18-27 [doi]
- 2: Satisfiability Checking Meets Symbolic Computation - (Project Paper)Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm 0001. 28-43 [doi]
- Formalization of Normal Random Variables in HOLMuhammad Qasim, Osman Hasan, Maissa Elleuch, Sofiène Tahar. 44-59 [doi]
- Progress of Self-Archiving Within the DML Corpus, with a View Toward Community DynamicsFabian Müller, Olaf Teschke. 63-74 [doi]
- Accessing the Mizar Library with a Weakly Strict Mizar ParserAdam Naumowicz, Radoslaw Piliszek. 77-82 [doi]
- Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and SemanticsWilliam M. Farmer. 83-98 [doi]
- Extracting Higher-Order Goals from the Mizar Mathematical LibraryChad E. Brown, Josef Urban. 99-114 [doi]
- Interoperability in the OpenDreamKit Project: The Math-in-the-Middle ApproachPaul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry, Tom Wiesing. 117-131 [doi]
- Formal Dependability Modeling and Analysis: A SurveyWaqar Ahmed, Osman Hasan, Sofiène Tahar. 132-147 [doi]
- Extending E Prover with Similarity Based Clause Selection StrategiesJan Jakubuv, Josef Urban. 151-156 [doi]
- Enhancement of Mizar Texts with Transitivity Property of PredicatesArtur Kornilowicz. 157-162 [doi]