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 |