| 2016 | On Interpolation and Symbol Elimination in Theory Extensions. | Viorica Sofronie-Stokkermans |
| 2016 | Congruence Closure in Intensional Type Theory. | Daniel Selsam, Leonardo de Moura |
| 2016 | On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT. | Roberto Sebastiani, Patrick Trentin |
| 2016 | Colors Make Theories Hard. | Roberto Sebastiani |
| 2016 | Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving. | Stephan Schulz, Martin Mhrmann |
| 2016 | Model Finding for Recursive Functions in SMT. | Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
| 2016 | Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. | Andrew Reynolds |
| 2016 | Better Proof Output for Vampire. | Giles Reger |
| 2016 | Global Subsumption Revisited (Briefly). | Giles Reger, Martin Suda |
| 2016 | From Axioms to Proof Rules, then add Quantifiers. | Revantha Ramanayake |
| 2016 | Inducing Syntactic Cut-Elimination for Indexed Nested Sequents. | Revantha Ramanayake |
| 2016 | Logic & Proofs for Cyber-Physical Systems. | Andr Platzer |
| 2016 | Non-clausal Connection-based Theorem Proving in Intuitionistic First-Order Logic. | Jens Otten |
| 2016 | nanoCoP: A Non-clausal Connection Prover. | Jens Otten |
| 2016 | Subsumption Algorithms for Three-Valued Geometric Resolution. | Hans de Nivelle |
| 2016 | : A Resolution-Based Prover for Multimodal K. | Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 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 | Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers. | Tomer Libal, Alexander Steen |
| 2016 | On Checking Kripke Models for Modal Logic K. | Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail |
| 2016 | Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub. | Eugen Kuksa, Till Mossakowski |
| 2016 | LOIS: an Application of SMT Solvers. | Eryk Kopczynski, Szymon Torunczyk |
| 2016 | Super-Blocked Clauses. | Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere |
| 2016 | TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. | Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe |
| 2016 | On Intervals and Bounds in Bit-vector Arithmetic. | Mikols Janota, Christoph M. Wintersteiger |
| 2016 | Translating Scala Programs to Isabelle/HOL - System Description. | Lars Hupel, Viktor Kuncak |