| 2018 | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. | Florian Lonsing, Uwe Egly |
| 2018 | A Simple Semi-automated Proof Assistant for First-order Modal Logics. | Tomer Libal |
| 2018 | A Tableaux Calculus for Reducing Proof Size. | Michael Peter Lettmann, Nicolas Peltier |
| 2018 | Constructive Decision via Redundancy-Free Proof-Search. | Dominique Larchey-Wendling |
| 2018 | An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem. | Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail |
| 2018 | A FOOLish Encoding of the Next State Relations of Imperative Programs. | Evgenii Kotelnikov, Laura Kovcs, Andrei Voronkov |
| 2018 | Extended Resolution Simulates DRAT. | Benjamin Kiesl, Adrin Rebola-Pardo, Marijn J. H. Heule |
| 2018 | Enumerating Justifications Using Resolution. | Yevgeny Kazakov, Peter Skocovsk |
| 2018 | A Separation Logic with Data: Small Models and Automation. | Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher |
| 2018 | A Logical Framework with Commutative and Non-commutative Subexponentials. | Max I. Kanovich, Stepan L. Kuznetsov, Vivek Nigam, Andre Scedrov |
| 2018 | Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. | Nicolas Jeannerod, Ralf Treinen |
| 2018 | A SAT-Based Approach to Learn Explainable Decision Sets. | Alexey Ignatiev, Filipe Pereira, Nina Narodytska, Joo Marques-Silva |
| 2018 | Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics. | Ullrich Hustadt, Cludia Nalon, Clare Dixon |
| 2018 | Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing. | Pei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang |
| 2018 | Efficient Interpolation for the Theory of Arrays. | Jochen Hoenicke, Tanja Schindler |
| 2018 | Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. | Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish |
| 2018 | Cops and CoCoWeb: Infrastructure for Confluence Tools. | Nao Hirokawa, Julian Nagele, Aart Middeldorp |
| 2018 | An Abstraction-Refinement Framework for Reasoning with Large Theories. | Julio Csar Lpez-Hernndez, Konstantin Korovin |
| 2018 | Automated Reasoning About Key Sets. | Miika Hannula, Sebastian Link |
| 2018 | A New Probabilistic Algorithm for Approximate Model Counting. | Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma |
| 2018 | A New Probabilistic Algorithm for Approximate Model Counting. | Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma |
| 2018 | VolCE: An Efficient Tool for Solving #SMT(LA) Problems. | Cunjing Ge, Feifei Ma, Jian Zhang |
| 2018 | Labelled Connection-based Proof Search for Multiplicative Intuitionistic. | Didier Galmiche, Daniel Mry |
| 2018 | Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic. | Marcelo Finger, Sandro Preto |
| 2018 | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. | Katalin Fazekas, Fahiem Bacchus, Armin Biere |