| 437 | -- | 438 | Maria Paola Bonacina. Six Decades of Automated Reasoning: Papers in Memory of Larry Wos |
| 439 | -- | 461 | Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe. Larry Wos: Visions of Automated Reasoning |
| 463 | -- | 497 | Maria Paola Bonacina. Set of Support, Demodulation, Paramodulation: A Historical Perspective |
| 499 | -- | 539 | Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. A Comprehensive Framework for Saturation Theorem Proving |
| 541 | -- | 564 | Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret. Making Higher-Order Superposition Work |
| 565 | -- | 574 | Robert Veroff. A Wos Challenge Met |
| 575 | -- | 584 | Sophie Tourret, Christoph Weidenbach. A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column |
| 585 | -- | 610 | Andreas Lochbihler. A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory |
| 611 | -- | 637 | Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields |
| 639 | -- | 666 | Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon. Local is Best: Efficient Reductions to Modal Logic K |
| 667 | -- | 688 | Akihisa Yamada 0002. Tuple Interpretations for Termination of Term Rewriting |
| 689 | -- | 746 | Predrag Janicic, Julien Narboux. Theorem Proving as Constraint Solving with Coherent Logic |
| 747 | -- | 803 | David J. Pearce 0001, Mark Utting, Lindsay Groves. Verifying Whiley Programs with Boogie |
| 805 | -- | 844 | Joshua Meyers, David I. Spivak, Ryan Wisnesky. Fast Left Kan Extensions Using the Chase |
| 845 | -- | 860 | Dennis de Champeaux. Faster Linear Unification Algorithm |
| 861 | -- | 904 | Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha. Pardinus: A Temporal Relational Model Finder |
| 905 | -- | 952 | Mallku Soldevila, Beta Ziliani, Bruno Silvestre. From Specification to Testing: Semantics Engineering for Lua 5.2 |
| 953 | -- | 988 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot. Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL |
| 989 | -- | 1030 | Wilmer Ricciotti, James Cheney. A Formalization of SQL with Nulls |
| 1031 | -- | 1063 | Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón. Formalization of the Computational Theory of a Turing Complete Functional Language Model |
| 1065 | -- | 1095 | Jose Divasón, René Thiemann. A Formalization of the Smith Normal Form in Higher-Order Logic |
| 1097 | -- | 0 | Jose Divasón, René Thiemann. Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic |
| 1099 | -- | 0 | Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon. Correction to: Local is Best: Efficient Reductions to Modal Logic K |