| 2012 | Automated and Human Proofs in General Mathematics: An Initial Comparison. | Jesse Alama, Daniel Khlwein, Josef Urban |
| 2012 | The Permutative λ-Calculus. | Beniamino Accattoli, Delia Kesner |
| 2012 | Enfragmo: A System for Modelling and Solving Search Problems with Logic. | Amir Aavani, Xiongnan (Newman) Wu, Shahab Tasharrofi, Eugenia Ternovska, David G. Mitchell |
| 2010 | Satisfiability of Non-linear (Ir)rational Arithmetic. | Harald Zankl, Aart Middeldorp |
| 2010 | On Implementing Modular Complexity Analysis. | Harald Zankl, Martin Korp |
| 2010 | Automated Proof Compression by Invention of New Definitions. | Jir Vyskocil, David Stanovsk, Josef Urban |
| 2010 | Qex: Symbolic SQL Query Explorer. | Margus Veanes, Nikolai Tillmann, Jonathan de Halleux |
| 2010 | Symbolic Automata Constraint Solving. | Margus Veanes, Nikolaj S. Bjrner, Leonardo Mendona de Moura |
| 2010 | Resolution for Stochastic Boolean Satisfiability. | Tino Teige, Martin Frnzle |
| 2010 | PBINT, A Logic for Modelling Search Problems Involving Arithmetic. | Shahab Tasharrofi, Eugenia Ternovska |
| 2010 | The TPTP World - Infrastructure for Automated Reasoning. | Geoff Sutcliffe |
| 2010 | Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions. | Hannes Strass, Michael Thielscher |
| 2010 | A Prolog-based Proof Tool for Type-Theory TA-lambda and Implicational Intuitionistic-Logic. | L. Yohanes Stefanus, Ario Santoso |
| 2010 | The Nullness Analyser of julia. | Fausto Spoto |
| 2010 | Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. | Camilo Rocha, Jos Meseguer |
| 2010 | Bottom-Up Tree Automata with Term Constraints. | Andreas Reu, Helmut Seidl |
| 2010 | Gdel Logics - A Survey. | Norbert Preining |
| 2010 | Counting and Enumeration Problems with Bounded Treewidth. | Reinhard Pichler, Stefan Rmmele, Stefan Woltran |
| 2010 | A Sudoku-Solver for Large Puzzles using SAT. | Uwe Pfeiffer, Tomas Karnagel, Guido Scheffler |
| 2010 | Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. | Lawrence C. Paulson, Jasmin Christian Blanchette |
| 2010 | An Isabelle-Like Procedural Mode for HOL Light. | Petros Papapanagiotou, Jacques D. Fleuriot |
| 2010 | Atomic Cut Introduction by Resolution: Proof Structuring and Compression. | Bruno Woltzenlogel Paleo |
| 2010 | Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. | Friedrich Neurauter, Harald Zankl, Aart Middeldorp |
| 2010 | Relentful Strategic Reasoning in Alternating-Time Temporal Logic. | Fabio Mogavero, Aniello Murano, Moshe Y. Vardi |
| 2010 | Expansion Nets: Proof-Nets for Propositional Classical Logic. | Richard McKinley |