| 2015 | A Decision Procedure for (Co)datatypes in SMT Solvers. Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | A Formalisation of Finite Automata Using Hereditarily Finite Sets. Lawrence C. Paulson |
| 2015 | A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen |
| 2015 | A Uniform Substitution Calculus for Differential Dynamic Logic. André Platzer |
| 2015 | Abstract Interpretation as Automated Deduction. Vijay D'Silva, Caterina Urban |
| 2015 | Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings Amy P. Felty, Aart Middeldorp |
| 2015 | Automated Reasoning in the Wild. Ulrich Furbach, Björn Pelzer, Claudia Schon |
| 2015 | Automated Theorem Proving for Assertions in Separation Logic with All Connectives. Zhe Hou, Rajeev Goré, Alwen Tiu |
| 2015 | Automating Leibniz's Theory of Concepts. Jesse Alama, Paul E. Oppenheimer, Edward N. Zalta |
| 2015 | Beagle - A Hierarchic Superposition Theorem Prover. Peter Baumgartner, Joshua Bax, Uwe Waldmann |
| 2015 | CTL Model Checking in Deduction Modulo. Kailiang Ji |
| 2015 | CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems. Kiraku Shintani, Nao Hirokawa |
| 2015 | Confluence Competition 2015. Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl |
| 2015 | Cooperating Proof Attempts. Giles Reger, Dmitry Tishkovsky, Andrei Voronkov |
| 2015 | Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers. Grant Olney Passmore |
| 2015 | Deciding ATL Amélie David |
| 2015 | Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. Haruhiko Sato, Sarah Winkler |
| 2015 | Exploring Theories with a Model-Finding Assistant. Salman Saghafi, Ryan Danas, Daniel J. Dougherty |
| 2015 | Expressing Symmetry Breaking in DRAT Proofs. Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2015 | History and Prospects for First-Order Automated Deduction. David A. Plaisted |
| 2015 | Inductive Beluga: Programming Proofs. Brigitte Pientka, Andrew Cave |
| 2015 | KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. Crystal Chang Din, Richard Bubel, Reiner Hähnle |
| 2015 | KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer |
| 2015 | Linear Integer Arithmetic Revisited. Martin Bromberger, Thomas Sturm, Christoph Weidenbach |
| 2015 | MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki |
| 2015 | Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent. Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa |
| 2015 | Playing with AVATAR. Giles Reger, Martin Suda, Andrei Voronkov |
| 2015 | Program Synthesis Using Dual Interpretation. Ashish Tiwari, Adrià Gascón, Bruno Dutertre |
| 2015 | Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3. Filip Maric, Predrag Janicic, Marko Malikovic |
| 2015 | Quantifier-Free Equational Logic and Prime Implicate Generation. Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2015 | Quantomatic: A Proof Assistant for Diagrammatic Reasoning. Aleks Kissinger, Vladimir Zamdzhiev |
| 2015 | Reducing Relative Termination to Dependency Pair Problems. José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada |
| 2015 | Regular Patterns in Second-Order Unification. Tomer Libal |
| 2015 | SEPIA: Search for Proofs Using Inferred Automata. Thomas Gransden, Neil Walkinshaw, Rajeev Raman |
| 2015 | SMTtoTPTP - A Converter for Theorem Proving Formats. Peter Baumgartner |
| 2015 | Stumbling Around in the Dark: Lessons from Everyday Mathematics. Ursula Martin |
| 2015 | System Description: E.T. 0.1. Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil |
| 2015 | Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition. Philippe Balbiani, Joseph Boudou |
| 2015 | Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies. Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai |
| 2015 | Termination Competition (termCOMP 2015). Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann |
| 2015 | The Lean Theorem Prover (System Description). Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |
| 2015 | Theorem Proving with Bounded Rigid E-Unification. Peter Backeman, Philipp Rümmer |
| 2015 | Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. Jan Gorzny, Bruno Woltzenlogel Paleo |