| Authors | Title | Paper | Talk |
|---|
| Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez and Albert Rubio | Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts |  | Aug 10 14:00 |
| Gilles Dowek | From the Universality of Mathematical Truth to the Interoperability of Proof Systems | | Aug 08 09:00 |
| Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli and Clark Barrett | Flexible Proof Production in an Industrial-Strength SMT Solver | | Aug 10 12:00 |
| Paolo Felli, Marco Montali and Sarah Winkler | CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic | | Aug 10 09:00 |
| Mauro Ferrari and Camillo Fiorentini | SAT-based Proof Search in Intermediate Propositional Logics | | Aug 08 16:00 |
| Hannes Ihalainen, Jeremias Berg and Matti Järvisalo | Clause Redundancy and Preprocessing in Maximum Satisfiability | | Aug 08 16:40 |
| Gereon Kremer, Andrew Reynolds, Clark Barrett and Cesare Tinelli | Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) | | Aug 08 10:00 |
| Joseph Reeves, Marijn Heule and Randal Bryant | Preprocessing of Propagation Redundant Clauses | | Aug 08 16:20 |
| Ying Sheng, Andres Noetzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare Tinelli | Reasoning About Vectors using an SMT Theory of Sequences | | Aug 10 11:40 |
| Martin Bromberger, Lorenz Leutgeb and Christoph Weidenbach | An Efficient Subsumption Test Pipeline for BS(LRA) Clauses | | Aug 08 12:00 |
| André Duarte and Konstantin Korovin | Ground Joinability and Connectedness in the Superposition Calculus | | Aug 08 11:20 |
| Fajar Haifani, Patrick Koopmann, Sophie Tourret and Christoph Weidenbach | Connection-Minimal Abduction in EL via Translation to FOL | | Aug 10 11:00 |
| Fajar Haifani and Christoph Weidenbach | Semantic Relevance | | Aug 09 14:35 |
| Hendrik Leidinger and Christoph Weidenbach | SCL(EQ): SCL for First-Order Logic with Equality | | Aug 08 11:00 |
| Akihisa Yamada | Term Ordering for Non-Reachability of (Conditional) Rewriting | | Aug 08 11:40 |
| Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann and Julián Méndez | Evonne: Interactive Proof Visualization for Description Logics (System Description) | | Aug 08 14:55 |
| Claudia Cauli, Magdalena Ortiz and Nir Piterman | Actions over Core-Closed Knowledge Bases | | Aug 08 14:00 |
| Tanel Tammet, Dirk Draheim and Priit Järv | GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) | | Aug 08 14:20 |
| Hui Yang, Yue Ma and Nicole Bidoit | Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications | | Aug 08 15:10 |
| Michael Bernreiter, Anela Lolic, Jan Maly and Stefan Woltran | Sequent Calculi for Choice Logics | | Aug 09 09:00 |
| Chad Brown and Cezary Kaliszyk | Lash 1.0 (System Description) | | Aug 09 09:20 |
| Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard and Hinde Bouziane | Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) | | Aug 09 09:35 |
| Štěpán Holub, Martin Raška and Štěpán Starosta | Binary Codes that do Not Preserve Primitivity | | Aug 09 10:10 |
| Takuya Matsuzaki and Tomohiro Fujita | Formula Simplification via Invariance Detection by Algebraically Indexed Types | | Aug 08 17:00 |
| Michał Sochański, Dorota Leszczyńska-Jasion, Szymon Chlebowski, Agata Tomczyk and Marcin Jukiewicz | Synthetic Tableaux: Minimal Tableau Search Heuristics | | Aug 09 09:50 |
| Marta Bilkova, Sabine Frittella and Daniil Kozhemiachenko | Paraconsistent Gödel Modal Logic | | Aug 10 16:20 |
| Eben Blaisdell, Max Kanovich, Stepan Kuznetsov, Elaine Pimentel and Andre Scedrov | Non-associative, Non-commutative Multi-Modal Linear Logic | | Aug 10 16:00 |
| Ori Lahav and Yoni Zohar | Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices | | Aug 10 16:40 |
| Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon | Local Reductions for the Modal Cube | | Aug 08 14:35 |
| Anupam Das and Marianna Girlando | Cyclic Proofs, Hypersequents, and Transitive Closure Logic | | Aug 09 11:40 |
| Francisco Durán, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer, Ruben Rubio and Carolyn Talcott | Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) | | Aug 09 14:55 |
| Andrzej Indrzejczak | Le\'sniewski's Ontology -- Proof-Theoretic Characterization | | Aug 09 11:20 |
| Chaitanya Mangla, Sean Holden and Paulson Larry | Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers | | Aug 09 14:00 |
| Temur Kutsia and Cleo Pau | A Framework for Approximate Generalization in Quantitative Theories | | Aug 09 15:10 |
| Jelle Piepenbrock, Tom Heskes, Mikolas Janota and Josef Urban | Guiding an Automated Theorem Prover with Neural Rewriting | | Aug 10 15:00 |
| Andrei Popescu | Rensets and Renaming-Based Recursion for Syntax with Bindings | | Aug 09 12:00 |
| Vitor Rodrigues Greati and Joao Marcos | Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics | | Aug 09 11:00 |
| Martin Suda | Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) | | Aug 09 14:20 |
| S. Akshay, Supratik Chakraborty and Debtanu Pal | On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices | | Aug 10 09:35 |
| Marius Bozga, Lucas Bueri and Radu Iosif | Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems | | Aug 10 11:20 |
| Florian Frohn and Jürgen Giesl | Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) | | Aug 10 09:55 |
| James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André Platzer | Implicit Definitions with Differential Equations for KeYmaera X (System Description) | | Aug 10 09:20 |
| Nils Lommen, Fabian Meyer and Jürgen Giesl | Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops | | Aug 10 10:10 |
