| 1 | -- | 2 | Jacques Carette, William M. Farmer. Preface |
| 3 | -- | 20 | Tobias Schmidt-Samoa. An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving |
| 21 | -- | 38 | Roy L. McCasland, Alan Bundy, Patrick F. Smith. Ascertaining Mathematical Theorems |
| 39 | -- | 56 | Jörn Ossowski, Christel Baier. Symbolic Reasoning with Weighted and Normalized Decision Diagrams |
| 57 | -- | 73 | David Delahaye, Micaela Mayero. Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System |
| 75 | -- | 91 | Luís Cruz-Filipe, Pierre Letouzey. A Large-Scale Experiment in Executing Extracted Programs |
| 93 | -- | 110 | Louise A. Dennis, Mateja Jamnik, Martin Pollet. On the Comparison of Proof Planning Systems: lambdaCLAM, Omega and IsaPlanner |
| 111 | -- | 125 | Ruth Hardy. Interactions Between PVS and Maple in Symbolic Analysis of Control Systems |
| 127 | -- | 142 | Martin Pollet, Volker Sorge. Connecting Logical Representations and Efficient Computations |
| 143 | -- | 160 | G. W. Hamilton. Poitín: Distilling Theorems From Conjectures |
| 161 | -- | 177 | Aurélie Hurault, Marc Pantel. Mathematical Service Trading Based on Equational Matching |