Editors: Laura Kovacs, Jasmin Blanchette and Dirk Pattinson

Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez and Albert RubioUsing Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart ContractsAug 10 14:00
Gilles DowekFrom the Universality of Mathematical Truth to the Interoperability of Proof SystemsAug 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 BarrettFlexible Proof Production in an Industrial-Strength SMT SolverAug 10 12:00
Paolo Felli, Marco Montali and Sarah WinklerCTL* Model Checking for Data-Aware Dynamic Systems with ArithmeticAug 10 09:00
Mauro Ferrari and Camillo FiorentiniSAT-based Proof Search in Intermediate Propositional LogicsAug 08 16:00
Hannes Ihalainen, Jeremias Berg and Matti JärvisaloClause Redundancy and Preprocessing in Maximum SatisfiabilityAug 08 16:40
Gereon Kremer, Andrew Reynolds, Clark Barrett and Cesare TinelliCooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description)Aug 08 10:00
Joseph Reeves, Marijn Heule and Randal BryantPreprocessing of Propagation Redundant ClausesAug 08 16:20
Ying Sheng, Andres Noetzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare TinelliReasoning About Vectors using an SMT Theory of SequencesAug 10 11:40
Martin Bromberger, Lorenz Leutgeb and Christoph WeidenbachAn Efficient Subsumption Test Pipeline for BS(LRA) ClausesAug 08 12:00
André Duarte and Konstantin KorovinGround Joinability and Connectedness in the Superposition CalculusAug 08 11:20
Fajar Haifani, Patrick Koopmann, Sophie Tourret and Christoph WeidenbachConnection-Minimal Abduction in EL via Translation to FOLAug 10 11:00
Fajar Haifani and Christoph WeidenbachSemantic RelevanceAug 09 14:35
Hendrik Leidinger and Christoph WeidenbachSCL(EQ): SCL for First-Order Logic with EqualityAug 08 11:00
Akihisa YamadaTerm Ordering for Non-Reachability of (Conditional) RewritingAug 08 11:40
Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann and Julián MéndezEvonne: Interactive Proof Visualization for Description Logics (System Description)Aug 08 14:55
Claudia Cauli, Magdalena Ortiz and Nir PitermanActions over Core-Closed Knowledge BasesAug 08 14:00
Tanel Tammet, Dirk Draheim and Priit JärvGK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)Aug 08 14:20
Hui Yang, Yue Ma and Nicole BidoitHypergraph-Based Inference Rules for Computing EL+-Ontology JustificationsAug 08 15:10
Michael Bernreiter, Anela Lolic, Jan Maly and Stefan WoltranSequent Calculi for Choice LogicsAug 09 09:00
Chad Brown and Cezary KaliszykLash 1.0 (System Description)Aug 09 09:20
Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard and Hinde BouzianeGoéland: A Concurrent Tableau-Based Theorem Prover (System Description)Aug 09 09:35
Štěpán Holub, Martin Raška and Štěpán StarostaBinary Codes that do Not Preserve PrimitivityAug 09 10:10
Takuya Matsuzaki and Tomohiro FujitaFormula Simplification via Invariance Detection by Algebraically Indexed TypesAug 08 17:00
Michał Sochański, Dorota Leszczyńska-Jasion, Szymon Chlebowski, Agata Tomczyk and Marcin JukiewiczSynthetic Tableaux: Minimal Tableau Search HeuristicsAug 09 09:50
Marta Bilkova, Sabine Frittella and Daniil KozhemiachenkoParaconsistent Gödel Modal LogicAug 10 16:20
Eben Blaisdell, Max Kanovich, Stepan Kuznetsov, Elaine Pimentel and Andre ScedrovNon-associative, Non-commutative Multi-Modal Linear LogicAug 10 16:00
Ori Lahav and Yoni ZoharEffective Semantics for the Modal Logics K and KT via Non-deterministic MatricesAug 10 16:40
Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare DixonLocal Reductions for the Modal CubeAug 08 14:35
Anupam Das and Marianna GirlandoCyclic Proofs, Hypersequents, and Transitive Closure LogicAug 09 11:40
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer, Ruben Rubio and Carolyn TalcottEquational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)Aug 09 14:55
Andrzej IndrzejczakLe\'sniewski's Ontology -- Proof-Theoretic CharacterizationAug 09 11:20
Chaitanya Mangla, Sean Holden and Paulson LarryBayesian Ranking for Strategy Scheduling in Automated Theorem ProversAug 09 14:00
Temur Kutsia and Cleo PauA Framework for Approximate Generalization in Quantitative TheoriesAug 09 15:10
Jelle Piepenbrock, Tom Heskes, Mikolas Janota and Josef UrbanGuiding an Automated Theorem Prover with Neural RewritingAug 10 15:00
Andrei PopescuRensets and Renaming-Based Recursion for Syntax with BindingsAug 09 12:00
Vitor Rodrigues Greati and Joao MarcosFinite Two-Dimensional Proof Systems for Non-finitely Axiomatizable LogicsAug 09 11:00
Martin SudaVampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)Aug 09 14:20
S. Akshay, Supratik Chakraborty and Debtanu PalOn Eventual Non-negativity and Positivity for the Weighted Sum of Powers of MatricesAug 10 09:35
Marius Bozga, Lucas Bueri and Radu IosifDecision Problems in a Logic for Reasoning about Reconfigurable Distributed SystemsAug 10 11:20
Florian Frohn and Jürgen GieslProving Non-Termination and Lower Runtime Bounds with LoAT (System Description)Aug 10 09:55
James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André PlatzerImplicit Definitions with Differential Equations for KeYmaera X (System Description)Aug 10 09:20
Nils Lommen, Fabian Meyer and Jürgen GieslAutomatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear LoopsAug 10 10:10