| 2018 | A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems. | Alireza Ensan, Eugenia Ternovska, Heng Liu |
| 2018 | A Generic Framework for Implicate Generation Modulo Theories. | Mnacho Echenim, Nicolas Peltier, Yanis Sellami |
| 2018 | Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs. | Gabriel Ebner, Matthias Schlaipfer |
| 2018 | Well-Founded Unions. | Jeremy E. Dawson, Nachum Dershowitz, Rajeev Gor |
| 2018 | Focussing, MALL and the Polynomial Hierarchy. | Anupam Das |
| 2018 | Cubicle- | Sylvain Conchon, David Declerck, Fatiha Zadi |
| 2018 | Efficient Encodings of First-Order Horn Formulas in Equational Logic. | Koen Claessen, Nicholas Smallbone |
| 2018 | A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. | Stefan Ciobaca, Dorel Lucanu |
| 2018 | A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. | Martin Bromberger |
| 2018 | Complexity of Combinations of Qualitative Constraint Satisfaction Problems. | Manuel Bodirsky, Johannes Greiner |
| 2018 | Superposition with Datatypes and Codatatypes. | Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard |
| 2018 | Set of Support for Higher-Order Reasoning. | Ahmed Bhayat, Giles Reger |
| 2018 | Superposition for Lambda-Free Higher-Order Logic. | Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann |
| 2018 | Pseudo-Propositional Logic. | Ahmad-Saher Azizi-Sultan |
| 2018 | From Syntactic Proofs to Combinatorial Proofs. | Matteo Acclavio, Lutz Straburger |
| 2018 | Reasoning About Exceptions in Ontologies: from the Lexicographic Closure to the Skeptical Closure. | Laura Giordano, Valentina Gliozzi |
| 2017 | Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. | Zhaowei Xu, Taolue Chen, Zhilin Wu |
| 2017 | Do Portfolio Solvers Harm? | Christoph Weidenbach |
| 2017 | AI at CADE/IJCAR. | Josef Urban |
| 2017 | Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. | Andreas Teucke, Christoph Weidenbach |
| 2017 | Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. | Gadi Tellez, James Brotherston |
| 2017 | Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. | Christian Sternagel, Thomas Sternagel |
| 2017 | Towards Logic-Based Verification of JavaScript Programs. | Jos Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene |
| 2017 | Challenges for Fast Synthesis Procedures in SMT. | Andrew Reynolds |
| 2017 | A Report of ARCADE 2017. | Giles Reger, Dmitriy Traytel |