| 2016 | : A Resolution-Based Prover for Multimodal K. Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
| 2016 | A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. Xincai Gu, Taolue Chen, Zhilin Wu |
| 2016 | A Logical Framework for Developing and Mechanizing Set Theories. Arnon Avron |
| 2016 | A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2016 | A Tableau System for Quasi-Hybrid Logic. Diana Costa, Manuel A. Martins |
| 2016 | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2016 | Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings Nicola Olivetti, Ashish Tiwari |
| 2016 | Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn L. Talcott |
| 2016 | Colors Make Theories Hard. Roberto Sebastiani |
| 2016 | Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition. Joseph Boudou |
| 2016 | Congruence Closure in Intensional Type Theory. Daniel Selsam, Leonardo de Moura |
| 2016 | Counting Constraints in Flat Array Fragments. Francesco Alberti, Silvio Ghilardi, Elena Pagani |
| 2016 | Effective Normalization Techniques for HOL. Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller |
| 2016 | Fast Cube Tests for LIA Constraint Solving. Martin Bromberger, Christoph Weidenbach |
| 2016 | Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. Yoni Zohar, Anna Zamansky |
| 2016 | Inducing Syntactic Cut-Elimination for Indexed Nested Sequents. Revantha Ramanayake |
| 2016 | Internal Guidance for Satallax. Michael Färber, Chad E. Brown |
| 2016 | Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
| 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 | Intuitionistic Layered Graph Logic. Simon Docherty, David J. Pym |
| 2016 | Logic & Proofs for Cyber-Physical Systems. André Platzer |
| 2016 | Lower Runtime Bounds for Integer Programs. Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, Jürgen Giesl |
| 2016 | Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. Jeremy E. Dawson, James Brotherston, Rajeev Goré |
| 2016 | Model Checking Parameterised Multi-token Systems via the Composition Method. Benjamin Aminof, Sasha Rubin |
| 2016 | Model Finding for Recursive Functions in SMT. Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
| 2016 | Nominal Confluence Tool. Takahito Aoto, Kentaro Kikuchi |
| 2016 | On Interpolation and Symbol Elimination in Theory Extensions. Viorica Sofronie-Stokkermans |
| 2016 | Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving. Stephan Schulz, Martin Möhrmann |
| 2016 | Programming by Examples: Applications, Algorithms, and Ambiguity Resolution. Sumit Gulwani |
| 2016 | Race Against the Teens - Benchmarking Mechanized Math on Pre-university Problems. Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai, Noriko H. Arai |
| 2016 | Schematic Cut Elimination and the Ordered Pigeonhole Principle. David M. Cerna, Alexander Leitsch |
| 2016 | Selecting the Selection. Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov |
| 2016 | Subsumption Algorithms for Three-Valued Geometric Resolution. Hans de Nivelle |
| 2016 | Super-Blocked Clauses. Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere |
| 2016 | System Description: GAPT 2.0. Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, Sebastian Zivota |
| 2016 | Translating Scala Programs to Isabelle/HOL - System Description. Lars Hupel, Viktor Kuncak |
| 2016 | Unbounded-Thread Program Verification using Thread-State Equations. Konstantinos Athanasiou, Peizun Liu, Thomas Wahl |
| 2016 | nanoCoP: A Non-clausal Connection Prover. Jens Otten |
| 2016 | raSAT: An SMT Solver for Polynomial Constraints. Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa |