Accepted Papers

Jesús Aransay, Laureano Lambán and Julio Rubio. Evasiveness through Binary Decision Diagrams

Mauricio Ayala-Rincón, Maribel Fernandez, Gabriel Ferreira Silva, Temur Kutsia and Daniele Nantes-Sobrinho. Nominal AC-Matching

Jonas Bayer, Alexey Gonus, Christoph Benzmüller and Dana Scott. Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation

Marc Berges, Jonas Betzendahl, Abhishek Chugh, Michael Kohlhase, Dominic Lohr and Dennis Müller. Learning Support Systems based on Mathematical Knowledge Management

Christopher Brown, Zoltán Kovács, Tomas Recio, Robert Vajda and M. Pilar Velez. GeoGebra Discovery (system entry)

Marco B. Caminati. Isabelle Formalisation of Original Representation Theorems

Robert Corless, David J. Jeffrey and Azar Shakoori. Teaching Linear Algebra in a mechanized mathematical environment

James Davenport. Proving an Execution of an Algorithm Correct?

Neeraj Gangwar and Nickvash Kani. Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems

Henry Hammer, Nanako Noda and Christopher Stone. ProofLang: the Language of arXiv Proofs

Simone Heisinger and Martina Seidl. True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers

John Hester, Briland Hitaj, Grant Passmore, Sam Owre, Natarajan Shankar and Eric Yeh. An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning

Fabian Huch and Yiannos Stathopoulos. Formalization Quality in Isabelle

Jan Jakubuv and Cezary Kaliszyk. VizAR: Visualization of Automated Reasoning Proofs.

Aabid Seeyal Abdul Kharim, T.V.H. Prathamesh, Shweta Rajiv and Rishi Vyas. Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem

Adam Naumowicz. Extending Numeric Automation for Number Theory Formalizations in Mizar

Florian Rabe and Stephen Watt. Extracting Theory Graphs from the Aldor Library

Florian Rabe and Franziska Weber. Morphism Equality in Theory Graphs

Jan Frederik Schaefer and Michael Kohlhase. Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters

Jeffrey Shallit. Proving Results About OEIS Sequences with Walnut

Mohit Tekriwal, Andrew Appel, Ariel Kellison, David Bindel and Jean-Baptiste Jeannin.   Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method

Eric Wieser.   Multiple-inheritance hazards in dependently-typed algebraic hierarchies

Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener and Natarajan Shankar. CoProver: A Recommender System for Proof Construction