| 2015 | A Formalisation of Finite Automata Using Hereditarily Finite Sets. | Lawrence C. Paulson |
| 2015 | Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers. | Grant Olney Passmore |
| 2015 | The Lean Theorem Prover (System Description). | Leonardo Mendona de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |
| 2015 | Stumbling Around in the Dark: Lessons from Everyday Mathematics. | Ursula Martin |
| 2015 | Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3. | Filip Maric, Predrag Janicic, Marko Malikovic |
| 2015 | Regular Patterns in Second-Order Unification. | Tomer Libal |
| 2015 | Reasoning About Loops Using Vampire. | Laura Kovcs, Simon Robillard |
| 2015 | Quantomatic: A Proof Assistant for Diagrammatic Reasoning. | Aleks Kissinger, Vladimir Zamdzhiev |
| 2015 | System Description: E.T. 0.1. | Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jir Vyskocil |
| 2015 | CTL Model Checking in Deduction Modulo. | Kailiang Ji |
| 2015 | Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies. | Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai |
| 2015 | Reducing Relative Termination to Dependency Pair Problems. | Jos Iborra, Naoki Nishida, Germn Vidal, Akihisa Yamada |
| 2015 | Automated Theorem Proving for Assertions in Separation Logic with All Connectives. | Zhe Hou, Rajeev Gor, Alwen Tiu |
| 2015 | Weak Completion Semantics and its Applications in Human Reasoning. | Steffen Hlldobler |
| 2015 | Expressing Symmetry Breaking in DRAT Proofs. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2015 | Using Vampire in Soundness Proofs of Type Systems. | Sylvia Grewe, Sebastian Erdweg, Mira Mezini |
| 2015 | SEPIA: Search for Proofs Using Inferred Automata. | Thomas Gransden, Neil Walkinshaw, Rajeev Raman |
| 2015 | Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. | Jan Gorzny, Bruno Woltzenlogel Paleo |
| 2015 | Termination Competition (termCOMP 2015). | Jrgen Giesl, Frdric Mesnard, Albert Rubio, Ren Thiemann, Johannes Waldmann |
| 2015 | Automated Reasoning in the Wild. | Ulrich Furbach, Bjrn Pelzer, Claudia Schon |
| 2015 | Tackling Benchmark Problems of Commonsense Reasoning. | Ulrich Furbach, Andrew S. Gordon, Claudia Schon |
| 2015 | KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. | Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Vlp, Andr Platzer |
| 2015 | Quantifier-Free Equational Logic and Prime Implicate Generation. | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
| 2015 | Abstract Interpretation as Automated Deduction. | Vijay D'Silva, Caterina Urban |
| 2015 | KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. | Crystal Chang Din, Richard Bubel, Reiner Hhnle |