Abstract is missing.
- Mining the Archive of Formal ProofsJasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow. 3-17 [doi]
- Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based RetrievalRichard Zanibbi, Awelemdy Orakwue. 18-36 [doi]
- Towards Formal Fault Tree Analysis Using Theorem ProvingWaqar Ahmed, Osman Hasan. 39-54 [doi]
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated ProofLuís Cruz-Filipe, Peter Schneider-Kamp. 55-70 [doi]
- A First Class Boolean Sort in First-Order Theorem Proving and TPTPEvgenii Kotelnikov, Laura Kovács, Andrei Voronkov. 71-86 [doi]
- Type Inference for ZFHSteven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall. 87-101 [doi]
- Generic LiteralsFlorian Rabe. 102-117 [doi]
- Ranking/Unranking of Lambda Terms with Compressed de Bruijn IndicesPaul Tarau. 118-133 [doi]
- A Flexiformal Model of Knowledge Dissemination and Aggregation in MathematicsMihnea Iancu, Michael Kohlhase. 137-152 [doi]
- Structure Formation in Large TheoriesSerge Autexier, Dieter Hutter. 155-170 [doi]
- Formal Logic Definitions for Interchange LanguagesFulya Horozal, Florian Rabe. 171-186 [doi]
- Math Literate Knowledge Management via Induced MaterialMihnea Iancu, Michael Kohlhase. 187-202 [doi]
- Strategies for Parallel MarkupBruce R. Miller. 203-210 [doi]
- Readable Formalization of Euler's Partition Theorem in MizarKarol Pak. 211-226 [doi]
- Automating Change of Representation for Proofs in Discrete MathematicsDaniel Raggi, Alan Bundy, Gudmund Grov, Alison Pease. 227-242 [doi]
- Performance Evaluation and Optimization of Math-Similarity SearchQun Zhang, Abdou Youssef. 243-257 [doi]
- Mizar: State-of-the-art and BeyondGrzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban. 261-279 [doi]
- Growing the Digital Repository of Mathematical Formulae with Generic SourcesHoward S. Cohl, Moritz Schubotz, Marjorie A. McClain, Bonita V. Saunders, Cherry Y. Zou, Azeem S. Mohammed, Alex A. Danoff. 280-287 [doi]
- Formalizing Physics: Automation, Presentation and Foundation IssuesCezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar. 288-295 [doi]
- A Survey on Retrieval of Mathematical KnowledgeFerruccio Guidi, Claudio Sacerdoti Coen. 296-315 [doi]
- Towards the Formalization of Fractional Calculus in Higher-Order LogicUmair Siddique, Osman Hasan, Sofiène Tahar. 316-324 [doi]
- LeoPARD - A Generic Platform for the Implementation of Higher-Order ReasonersMax Wisniewski, Alexander Steen, Christoph Benzmüller. 325-330 [doi]
- TIP: Tons of Inductive ProblemsKoen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone. 333-337 [doi]
- Semantic Enrichment of Mathematics via 'tooltips'Ross Moore. 338-342 [doi]
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar LibraryKazuhisa Nakasho, Yasunari Shidama. 343-347 [doi]
- Tools for MML Environment AnalysisAdam Naumowicz. 348-352 [doi]
- Enabling Symbolic and Numerical Computations in HOL LightOns Seddiki, Cvetan Dunchev, Sanaz Khan Afshar, Sofiène Tahar. 353-358 [doi]