| 2018 | A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. Stefan Ciobaca, Dorel Lucanu |
| 2018 | A FOOLish Encoding of the Next State Relations of Imperative Programs. Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov |
| 2018 | A Generic Framework for Implicate Generation Modulo Theories. Mnacho Echenim, Nicolas Peltier, Yanis Sellami |
| 2018 | A Logical Framework with Commutative and Non-commutative Subexponentials. Max I. Kanovich, Stepan L. Kuznetsov, Vivek Nigam, Andre Scedrov |
| 2018 | A New Probabilistic Algorithm for Approximate Model Counting. Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma |
| 2018 | A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. Martin Bromberger |
| 2018 | A Resolution-Based Calculus for Preferential Logics. Cláudia Nalon, Dirk Pattinson |
| 2018 | A SAT-Based Approach to Learn Explainable Decision Sets. Alexey Ignatiev, Filipe Pereira, Nina Narodytska, João Marques-Silva |
| 2018 | A Separation Logic with Data: Small Models and Automation. Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher |
| 2018 | A Tableaux Calculus for Reducing Proof Size. Michael Peter Lettmann, Nicolas Peltier |
| 2018 | A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. Guillaume Melquiond, Raphaël Rieu-Helft |
| 2018 | ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. Bartosz Piotrowski, Josef Urban |
| 2018 | An Abstraction-Refinement Framework for Reasoning with Large Theories. Julio César López-Hernández, Konstantin Korovin |
| 2018 | An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem. Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail |
| 2018 | Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings Didier Galmiche, Stephan Schulz, Roberto Sebastiani |
| 2018 | Automated Reasoning About Key Sets. Miika Hannula, Sebastian Link |
| 2018 | Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. Étienne Payet, Fausto Spoto |
| 2018 | Complexity of Combinations of Qualitative Constraint Satisfaction Problems. Manuel Bodirsky, Johannes Greiner |
| 2018 | Constructive Decision via Redundancy-Free Proof-Search. Dominique Larchey-Wendling |
| 2018 | Cops and CoCoWeb: Infrastructure for Confluence Tools. Nao Hirokawa, Julian Nagele, Aart Middeldorp |
| 2018 | Cubicle- Sylvain Conchon, David Declerck, Fatiha Zaïdi |
| 2018 | Datatypes with Shared Selectors. Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett |
| 2018 | Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. Nicolas Jeannerod, Ralf Treinen |
| 2018 | Efficient Encodings of First-Order Horn Formulas in Equational Logic. Koen Claessen, Nicholas Smallbone |
| 2018 | Efficient Interpolation for the Theory of Arrays. Jochen Hoenicke, Tanja Schindler |
| 2018 | Efficient Model Construction for Horn Logic with VLog - System Description. Jacopo Urbani, Markus Krötzsch, Ceriel J. H. Jacobs, Irina Dragoste, David Carral |
| 2018 | Enumerating Justifications Using Resolution. Yevgeny Kazakov, Peter Skocovský |
| 2018 | Exploring Approximations for Floating-Point Arithmetic Using UppSAT. Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer |
| 2018 | Extended Resolution Simulates DRAT. Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule |
| 2018 | FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. Yizheng Zhao, Renate A. Schmidt |
| 2018 | FORT 2.0. Franziska Rapp, Aart Middeldorp |
| 2018 | Focussing, MALL and the Polynomial Hierarchy. Anupam Das |
| 2018 | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann |
| 2018 | From Syntactic Proofs to Combinatorial Proofs. Matteo Acclavio, Lutz Straßburger |
| 2018 | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. Katalin Fazekas, Fahiem Bacchus, Armin Biere |
| 2018 | Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing. Pei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang |
| 2018 | MædMax: A Maximal Ordered Completion Tool. Sarah Winkler, Georg Moser |
| 2018 | Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic. Marcelo Finger, Sandro Preto |
| 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 | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. Florian Lonsing, Uwe Egly |
| 2018 | Superposition for Lambda-Free Higher-Order Logic. Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann |
| 2018 | Superposition with Datatypes and Codatatypes. Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard |
| 2018 | The Higher-Order Prover Leo-III. Alexander Steen, Christoph Benzmüller |
| 2018 | Theories as Types. Dennis Müller, Florian Rabe, Michael Kohlhase |
| 2018 | Uniform Substitution for Differential Game Logic. André Platzer |
| 2018 | Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. Bohua Zhan, Maximilian P. L. Haslbeck |
| 2018 | Well-Founded Unions. Jeremy E. Dawson, Nachum Dershowitz, Rajeev Goré |