Automated deduction - CADE 30 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025 proceedings Clark Barrett, Uwe Waldmann, editors

Format:

Book

Conference/Event

Contributor:

Barrett, Clark, editor.

Waldmann, Uwe, editor.

Conference Name:

International Conference on Automated Deduction (30th : 2025 : Stuttgart, Germany)

Series:

Lecture notes in computer science ; 15943.

Lecture notes in computer science. Lecture notes in artificial intelligence

Lecture notes in computer science 1611-3349 15943

Lecture notes in artificial intelligence

Language:

English

Subjects (All):

Automatic theorem proving.

Genre:

proceedings (reports)

Conference papers and proceedings

Conference papers and proceedings.

Physical Description:

1 online resource

Place of Publication:

Cham, Switzerland Springer [2025]

Summary:

"This book constitutes the proceedings of the 30th International Conference on Automated Deduction, CADE 30, which took place in Stuttgart, Germany, during July 2025. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The 33 full papers and 4 short papers included in these proceedings were carefully reviewed and selected from 87 submissions. They were organized in topical sections on SMT; rewriting; formalizations in Isabelle/HOL; calculi; machine learning for automated deduction; model checking and quantifier elimination; saturation; equational reasoning; non-classical logics; and SAT"-- Springer Nature Link

Contents:

Choose your proofs : commutativity and symmetry for smarter reasoning / Azadeh Farzan

Being polite is not enough (and other limits of theory combination) / Guilherme V. Toledo, Benjamin Przybocki, and Yoni Zohar

On symbol elimination and uniform interpolation in theory extensions / Viorica Sofronie-Stokkermans

What’s decidable about arrays with sums? / Roland Herrmann and Philipp Rümmer

Cazamariposas : automated instability debugging in SMT-based program verification / Yi Zhou, Amar Shah, Zhengyao Lin, Marijn J. H. Heule, and Bryan Parno

Boosting MCSAT modulo nonlinear integer arithmetic via local search / Enrico Lipparini, Thomas Hader, Ahmed Irfan, and Stéphane Graham-Lengrand

More is less : adding polynomials for faster explanations in NLSAT / Valentin Promies, Jasper Nalbach, Erika Ábrahám, and Paul Wagner

Ground truth : checking Vampire proofs via satisfiability modulo theories / Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, and Anja Petkovic Komel

SMT and functional equation solving over the reals : challenges from the IMO / Chad E. Brown, Karel Chvalovský, Mikoláš Janota, Mirek Olšák, and Stefan Ratschan

Lexicographic combination of reduction pairs / Teppei Saito and Nao Hirokawa

Confluence of almost parallel-closed generalized term rewriting systems / Salvador Lucas

The computability path order for beta-eta-normal higher-order rewriting / Johannes Niederhauser and Aart Middeldorp

Sort-based confluence criteria for non-left-linear higher-order rewriting / Thiago Felicissimo and Jean-Pierre Jouannaud

Verified path indexing / Mohamed Chaabani and Simon Robillard

Simplified and verified : a second look at a proof-producing union-find algorithm / Lukas Stevens and Rebecca Ghidini

Faithful logic embeddings in HOL—deep and shallow / Christoph Benzmüller

A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution / Martin Bromberger, Martin Desharnais, and Christoph Weidenbach

Interoperability of proof systems with SC-TPTP / Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, and Viktor Kuncak

Cut elimination for negative free logics with definite descriptions / Andrzej Indrzejczak

From modal sequent calculi to modal resolution / Dirk Pattinson, Cláudia Nalon, and Sourabh Peruri

A fresh inductive approach to useful call-by-value / Pablo Barenbaum, Delia Kesner, and Mariana Milicich

Efficient neural clause-selection reinforcement / Martin Suda

Learning conjecturing from scratch / Thibault Gauthier and Josef Urban

A theorem prover based approach for SAT-based model checking certification / Giulia Sindoni, Paolo Pasini, Gianpiero Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, and Stefano Tonetta

Infinite state model checking by learning transitive relations / Florian Frohn and Jürgen Giesl

Relatively complete and efficient partial quantifier elimination / Estifanos Getachew, Arie Gurfinkel, and Richard Trefler

Computing witnesses using the SCAN algorithm / Fabian Achammer, Stefan Hetzl, and Renate A. Schmidt

Partial redundancy in saturation / Márton Hajdu, Laura Kovács, and Andrei Voronkov

Term ordering diagrams / Márton Hajdu, Robin Coutelier, Laura Kovács, and Andrei Voronkov

Exploiting instantiations from paramodulation proofs in Isabelle/HOL / Lukas Bartl, Jasmin Blanchette, and Tobias Nipkow

Computing ground congruence classes / Hendrik Leidinger and Christoph Weidenbach

Anti-pattern templates / Jan Otop

Equational reasoning modulo commutativity in languages with binders / Ali K. Caires-Santos, Maribel Fernández, and Daniele Nantes-Sobrinho

Uniform interpolation and forgetting for large-scale ontologies with application to semantic difference in SNOMED CT / Yizheng Zhao, Junyi Zhang, and Renate A. Schmidt

Concrete domains meet expressive cardinality restrictions in description logics / Franz Baader, Stefan Borgwardt, Filippo De Bortoli, and Patrick Koopmann

A real-analytic approach to differential-algebraic dynamic logic / Jonathan Hellwig and André Platzer

Entailment vs. verification for partial-assignment satisfiability and enumeration / Roberto Sebastiani

Unfolding boxes with local constraints / Long Qian, Eric Wang, Bernardo Subercaseaux, and Marijn J. H. Heule

Correction to : automated deduction – CADE 30 / Clark Barrett and Uwe Waldmann

Notes:

Includes bibliographical references and index

Online resource; title from PDF title page (Springer Nature Link, viewed June 22, 2026)

Other Format:

Print version International Conference on Automated Deduction (30th : 2025 : Stuttgart, Germany) Automated deduction - CADE 30

ISBN:

9783031999840

3031999843

OCLC:

1530513316

Access Restriction:

Some versions Open access versions available from some providers open access