| 2014 | In Which Sense Is Fuzzy Logic a Logic for Vagueness? | Libor Behounek |
| 2014 | OTTER Proofs in Tarskian Geometry. | Michael Beeson, Larry Wos |
| 2014 | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories. | Joshua Bax |
| 2014 | Finite Quantification in Hierarchic Theorem Proving. | Peter Baumgartner, Joshua Bax, Uwe Waldmann |
| 2014 | From Reachability to Temporal Specifications in Cost-Sharing Games. | Guy Avni, Orna Kupferman, Tami Tamir |
| 2014 | Learning Preferences for Collaboration. | Eva Armengol |
| 2014 | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics. | Negin Arhami, Geoff Sutcliffe |
| 2014 | The Fractal Dimension of SAT Formulas. | Carlos Anstegui, Maria Luisa Bonet, Jess Girldez-Cru, Jordi Levy |
| 2014 | Dialogues for proof search. | Jesse Alama |
| 2014 | Multi-Attribute Decision Making using Weighted Description Logics. | Erman Acar, Christian Meilicke |
| 2013 | Propositional Temporal Proving with Reductions to a SAT Problem. | Richard Williams, Boris Konev |
| 2013 | Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems. | Viorica Sofronie-Stokkermans |
| 2013 | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. | Steffen Juilf Smolka, Jasmin Christian Blanchette |
| 2013 | Automated Reasoning, Fast and Slow. | Natarajan Shankar |
| 2013 | Quantifier Instantiation Techniques for Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
| 2013 | Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. | Leonardo Mendona de Moura, Grant Olney Passmore |
| 2013 | A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies. | Marta Cialdea Mayer |
| 2013 | A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. | Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika brahm, Bernd Becker |
| 2013 | Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. | Ramana Kumar |
| 2013 | E-MaLeS 1.1. | Daniel Khlwein, Stephan Schulz, Josef Urban |
| 2013 | : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. | Gergely Kovsznai, Andreas Frhlich, Armin Biere |
| 2013 | Completeness and Decidability Results for First-Order Clauses with Indices. | Abdelkader Kersani, Nicolas Peltier |
| 2013 | Extended Resolution as Certificates for Propositional Logic. | Chantal Keller |
| 2013 | InKreSAT: Modal Reasoning via Incremental Reduction to SAT. | Mark Kaminski, Tobias Tebbi |
| 2013 | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. | Cezary Kaliszyk, Josef Urban |