| 2026 | A Complete Proof System for HyperLTL. | Naijun Zhan, Wen Tang, Dimitar P. Guelev |
| 2026 | Complexity and Expressivity of the Uniform Fluted Fragment. | Hongkai Yin |
| 2026 | Saving Craig in the Fluted Fragment. | Hongkai Yin |
| 2026 | Generating Theorems by Generating Proof Structures. | Christoph Wernhard |
| 2026 | Complete Robust Hybrid Systems Reachability. | Noah Abou El Wafa, Andr Platzer |
| 2026 | Bringing Closure to Theory Combination Properties. | Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar |
| 2026 | On Constructing Most General Solutions for Parametric Constraints. | Viorica Sofronie-Stokkermans |
| 2026 | Pgeon: Generating Tableau-Based Provers from Declarative Specifications of Logical Calculi. | Romain Sidhoum, Simon Robillard, David Delahaye |
| 2026 | Finite Model Finding in First-Order Modal Logics. | Happy Khairunnisa Sariyanto, Alexander Steen, Geoff Sutcliffe |
| 2026 | Ordered Adjoint Logic. | Sophia Roshal, Frank Pfenning |
| 2026 | Ethos: A Fast Proof Checker for the Eunoia Logical Framework. | Andrew Reynolds, Hans-Jrg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | A General Approach for SMT Proof Skeletons. | Joseph E. Reeves, Haniel Barbosa, Andrew Reynolds, Marijn J. H. Heule |
| 2026 | Semantics for Dependently-Typed HOL. | Florian Rabe |
| 2026 | The Termination of Nielsen Transformations Applied to Word Equations with Length Constraints. | Benjamin Przybocki, Clark W. Barrett |
| 2026 | Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements. | Enguerrand Prebet, Andr Platzer |
| 2026 | A Unified Formalization of Context-Free Grammar Theory. | Tobias Nipkow, Fabian Lehr, Moritz Roos, Akihisa Yamada |
| 2026 | Unification of Deterministic Higher-Order Patterns. | Johannes Niederhauser, Aart Middeldorp |
| 2026 | grind: An SMT-Inspired Tactic for Lean 4 (Short Paper - System Description). | Kim Morrison, Leonardo de Moura |
| 2026 | Implementing Fuzzy OSF Logic Unification and Normalization (Short Paper). | Gian Carlo Milanese, Gabriella Pasi |
| 2026 | Automatic Abstraction Refinement for Hyperproperties Verification. | Malak Marrid, Shachar Itzhaky, Sharon Shoham, Yakir Vizel |
| 2026 | Complexity of Reasoning in Kleene Algebra with Sum-of-Letters Hypotheses. | Stepan L. Kuznetsov |
| 2026 | Tao's Equational Proof Challenge Accepted. | Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule |
| 2026 | SMT-Based Deontic Reasoning for qvist Logics. | Christian Kll, Agata Ciabattoni, Dmitry Rozplokhas |
| 2026 | Formally Verified Graph Generation with SAT Modulo Symmetries and Lean. | Markus Kirchweger, Pablo Manrique, Stefan Szeider |
| 2026 | Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks. | Jan-Christoph Kassing, Henri Nagel, Alexander Schlecht, Jrgen Giesl |