| 2016 | Optimizing Inconsistency-tolerant Description Logic Reasoning. | Mokarrom Hossain, Wendy MacCaull |
| 2016 | Selecting the Selection. | Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov |
| 2016 | Deduction as a Service. | Mohamed Hassona, Stephan Schulz |
| 2016 | Programming by Examples: Applications, Algorithms, and Ambiguity Resolution. | Sumit Gulwani |
| 2016 | A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. | Xincai Gu, Taolue Chen, Zhilin Wu |
| 2016 | Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny. | Sylvia Grewe, Sebastian Erdweg, Mira Mezini |
| 2016 | Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. | Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
| 2016 | Lower Runtime Bounds for Integer Programs. | Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, Jrgen Giesl |
| 2016 | No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. | Michael Frber, Cezary Kaliszyk |
| 2016 | Internal Guidance for Satallax. | Michael Frber, Chad E. Brown |
| 2016 | System Description: GAPT 2.0. | Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, Sebastian Zivota |
| 2016 | Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. | Francisco Durn, Steven Eker, Santiago Escobar, Narciso Mart-Oliet, Jos Meseguer, Carolyn L. Talcott |
| 2016 | Intuitionistic Layered Graph Logic. | Simon Docherty, David J. Pym |
| 2016 | Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. | Jeremy E. Dawson, James Brotherston, Rajeev Gor |
| 2016 | A Tableau System for Quasi-Hybrid Logic. | Diana Costa, Manuel A. Martins |
| 2016 | Sequent Calculi for Indexed Epistemic Logics. | Giovanna Corsi, Eugenio Orlandelli |
| 2016 | Alternative Treatments of Common Binary Relations in First-order Automated Reasoning. | Koen Claessen, Ann Lilliestrm |
| 2016 | Theory-Specific Reasoning about Loops with Arrays using Vampire. | Yuting Chen, Laura Kovcs, Simon Robillard |
| 2016 | Schematic Cut Elimination and the Ordered Pigeonhole Principle. | David M. Cerna, Alexander Leitsch |
| 2016 | Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. | Martin Bromberger, Christoph Weidenbach |
| 2016 | Fast Cube Tests for LIA Constraint Solving. | Martin Bromberger, Christoph Weidenbach |
| 2016 | Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments. | Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala |
| 2016 | Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition. | Joseph Boudou |
| 2016 | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2016 | Satisfiability Modulo Free Data Structures Combined with Bridging Functions. | Raphal Berthon, Christophe Ringeissen |