Skip to main content

CADE-30 Accepted Papers

Lukas Bartl, Jasmin Blanchette and Tobias Nipkow. Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Fabian Achammer, Stefan Hetzl and Renate A. Schmidt. Computing Witnesses Using the SCAN Algorithm
Teppei Saito and Nao Hirokawa. Lexicographic Combination of Reduction Pairs
Gianpiero Cabodi, Paolo Enrico Camurati, Alberto Griggio, Marco Palena, Paolo Pasini, Marco Roveri, Giulia Sindoni and Stefano Tonetta. A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Florian Frohn and Jürgen Giesl. Infinite State Model Checking by Learning Transitive Relations
Johannes Niederhauser and Aart Middeldorp. The Computability Path Ordering for Beta-Eta-Normal Higher-Order Rewriting
Lukas Stevens and Rebecca Ghidini. Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Thiago Felicissimo and Jean-Pierre Jouannaud. Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Salvador Lucas. Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Martin Suda. Efficient Neural Clause-Selection Reinforcement
Estifanos Getachew, Arie Gurfinkel and Richard Trefler. Relatively Complete and Efficient Partial Quantifier Elimination
Yizheng Zhao and Renate A. Schmidt. Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Guilherme Toledo, Benjamin Przybocki and Yoni Zohar. Being polite is not enough (and other limits of theory combination)
Andrei Voronkov, Michael Rawson, Anja Petković Komel and Johannes Schoisswohl. Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Hendrik Leidinger and Christoph Weidenbach. Computing Ground Congruence Classes
Simon Guilloud, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak and Julie Cailler. Interoperability of Proof systems with SC-TPTP (System Description)
Andrzej Indrzejczak. Cut Elimination for Negative Free Logics with Definite Descriptions
Thibault Gauthier and Josef Urban. Learning Conjecturing from Scratch
Franz Baader, Stefan Borgwardt, Filippo De Bortoli and Patrick Koopmann. Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Pablo Barenbaum, Delia Kesner and Mariana Milicich. A Fresh Inductive Approach to Useful Call-by-Value
Chad Brown, Karel Chvalovský, Mikoláš Janota, Miroslav Olšák and Stefan Ratschan. SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner. More is Less: Adding Polynomials for Faster Explanations in NLSAT
Jan Otop. Anti-pattern templates
Mohamed Chaabani and Simon Robillard. Verified Path Indexing
Marton Hajdu, Laura Kovács and Andrei Voronkov. Partial Redundancy in Saturation
Christoph Benzmüller. Faithful Logic Embeddings in HOL – A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level
Roberto Sebastiani. Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Martin Bromberger, Martin Desharnais and Christoph Weidenbach. A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Roland Herrmann and Philipp Rümmer. What's Decidable About Arrays With Sums?
Viorica Sofronie-Stokkermans. On Symbol Elimination and Uniform Interpolation in Theory Extensions
Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand. Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Ali Khan Caires Ribeiro Santos, Maribel Fernandez and Daniele Nantes Sobrinho. Equational Reasoning Modulo Commutativity in Languages with Binders
Dirk Pattinson, Cláudia Nalon and Sourabh Peruri. From Modal Sequent Calculi to Modal Resolution
Jonathan Hellwig and André Platzer. A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Long Qian, Eric Wang, Bernardo Subercaseaux and Marijn Heule. Unfolding Boxes with Local Constraints
Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule and Bryan Parno. Cazamariposas: Automated Instability Debugging in SMT-based Program Verification