Abstract is missing.
- Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart ContractsElvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, Albert Rubio. 3-7 [doi]
- From the Universality of Mathematical Truth to the Interoperability of Proof SystemsGilles Dowek. 8-11 [doi]
- Flexible Proof Production in an Industrial-Strength SMT SolverHaniel Barbosa, Andrew Reynolds 0001, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett. 15-35 [doi]
- * Model Checking for Data-Aware Dynamic Systems with ArithmeticPaolo Felli, Marco Montali, Sarah Winkler. 36-56 [doi]
- SAT-Based Proof Search in Intermediate Propositional LogicsCamillo Fiorentini, Mauro Ferrari 0002. 57-74 [doi]
- Clause Redundancy and Preprocessing in Maximum SatisfiabilityHannes Ihalainen, Jeremias Berg, Matti Järvisalo. 75-94 [doi]
- Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)Gereon Kremer, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli. 95-105 [doi]
- Preprocessing of Propagation Redundant ClausesJoseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant. 106-124 [doi]
- Reasoning About Vectors Using an SMT Theory of SequencesYing Sheng 0007, Andres Nötzli, Andrew Reynolds 0001, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli. 125-143 [doi]
- An Efficient Subsumption Test Pipeline for BS(LRA) ClausesMartin Bromberger, Lorenz Leutgeb, Christoph Weidenbach. 147-168 [doi]
- Ground Joinability and Connectedness in the Superposition CalculusAndré Duarte 0002, Konstantin Korovin. 169-187 [doi]
- EL via Translation to FOLFajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach. 188-207 [doi]
- Semantic RelevanceFajar Haifani, Christoph Weidenbach. 208-227 [doi]
- SCL(EQ): SCL for First-Order Logic with EqualityHendrik Leidinger, Christoph Weidenbach. 228-247 [doi]
- Term Orderings for Non-reachability of (Conditional) RewritingAkihisa Yamada 0002. 248-267 [doi]
- Evonne: Interactive Proof Visualization for Description Logics (System Description)Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann, Julián Méndez. 271-280 [doi]
- Actions over Core-Closed Knowledge BasesClaudia Cauli, Magdalena Ortiz, Nir Piterman. 281-299 [doi]
- GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)Tanel Tammet, Dirk Draheim, Priit Järv. 300-309 [doi]
- +-Ontology JustificationsHui Yang, Yue Ma, Nicole Bidoit. 310-328 [doi]
- Sequent Calculi for Choice LogicsMichael Bernreiter, Anela Lolic, Jan Maly 0001, Stefan Woltran. 331-349 [doi]
- Lash 1.0 (System Description)Chad E. Brown, Cezary Kaliszyk. 350-358 [doi]
- Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane. 359-368 [doi]
- Binary Codes that Do Not Preserve PrimitivityStepan Holub, Martin Raska, Stepán Starosta. 369-387 [doi]
- Formula Simplification via Invariance Detection by Algebraically Indexed TypesTakuya Matsuzaki, Tomohiro Fujita. 388-406 [doi]
- Synthetic Tableaux: Minimal Tableau Search HeuristicsMichal Sochanski, Dorota Leszczynska-Jasion, Szymon Chlebowski, Agata Tomczyk, Marcin Jukiewicz. 407-425 [doi]
- Paraconsistent Gödel Modal LogicMarta Bílková, Sabine Frittella, Daniil Kozhemiachenko. 429-448 [doi]
- Non-associative, Non-commutative Multi-modal Linear LogicEben Blaisdell, Max I. Kanovich, Stepan L. Kuznetsov, Elaine Pimentel, Andre Scedrov. 449-467 [doi]
- Effective Semantics for the Modal Logics K and KT via Non-deterministic MatricesOri Lahav, Yoni Zohar. 468-485 [doi]
- Local Reductions for the Modal CubeCláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon. 486-505 [doi]
- Cyclic Proofs, Hypersequents, and Transitive Closure LogicAnupam Das 0002, Marianna Girlando. 509-528 [doi]
- Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)Francisco Durán 0001, Steven Eker, Santiago Escobar 0001, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn L. Talcott. 529-540 [doi]
- Leśniewski's Ontology - Proof-Theoretic CharacterizationAndrzej Indrzejczak. 541-558 [doi]
- Bayesian Ranking for Strategy Scheduling in Automated Theorem ProversChaitanya Mangla, Sean B. Holden, Lawrence C. Paulson. 559-577 [doi]
- A Framework for Approximate Generalization in Quantitative TheoriesTemur Kutsia, Cleopatra Pau. 578-596 [doi]
- Guiding an Automated Theorem Prover with Neural RewritingJelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban. 597-617 [doi]
- Rensets and Renaming-Based Recursion for Syntax with BindingsAndrei Popescu 0001. 618-639 [doi]
- Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable LogicsVitor Greati, João Marcos 0001. 640-658 [doi]
- Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)Martin Suda 0001. 659-667 [doi]
- On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of MatricesS. Akshay 0001, Supratik Chakraborty, Debtanu Pal. 671-690 [doi]
- Decision Problems in a Logic for Reasoning About Reconfigurable Distributed SystemsMarius Bozga, Lucas Bueri, Radu Iosif. 691-711 [doi]
- Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)Florian Frohn, Jürgen Giesl. 712-722 [doi]
- Implicit Definitions with Differential Equations for KeYmaera X - (System Description)James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer. 723-733 [doi]
- Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear LoopsNils Lommen, Fabian Meyer, Jürgen Giesl. 734-754 [doi]