Ulteriori informazioni
Sommario
.- Invited Talks.
.- A Decade of Lean: Advancing Proof Automation for Mathematics and Software Verification.
.- Taming Infinity for Verification in First-Order Logic.
.- Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning.
.- SMT.
.- Being polite is not enough (and other limits of theory combination).
.- On Symbol Elimination and Uniform Interpolation in Theory Extensions.
.- What’s Decidable About Arrays With Sums?
.- Cazamariposas: Automated Instability Debugging in SMT-based Program Verification.
.- Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
.- More is Less: Adding Polynomials for Faster Explanations in NLSAT.
.- Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories.
.- SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
.- Rewriting.
.- Lexicographic Combination of Reduction Pairs.
.- Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems.
.- The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting.
.- Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting.
.- Formalizations in Isabelle/HOL.
.- Verified Path Indexing.
.- Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm.
.- Faithful Logic Embeddings in HOL – Deep and Shallow.
.- A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution.
.- Calculi.
.- Interoperability of Proof systems with SC-TPTP (System Description) .
.- Cut Elimination for Negative Free Logics with Definite Descriptions.
.- From Modal Sequent Calculi to Modal Resolution.
.- A Fresh Inductive Approach to Useful Call-by-Value.
.- Machine Learning for Automated Deduction.
.- Efficient Neural Clause-Selection Reinforcement.
.- Learning Conjecturing from Scratch.
.- Model Checking and Quantifier Elimination.
.- A Theorem Prover Based Approach for SAT-Based Model Checking Certification.
.- Infinite State Model Checking by Learning Transitive Relations.
.- Relatively Complete and Efficient Partial Quantifier Elimination.
.- Saturation.
.- Computing Witnesses Using the SCAN Algorithm.
.- Partial Redundancy in Saturation.
.- Term Ordering Diagrams.
.- Equational Reasoning.
.- Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL.
.- Computing Ground Congruence Classes.
.- Anti-pattern templates.
.- Equational Reasoning Modulo Commutativity in Languages with Binders.
.- Non-Classical Logics.
.- Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT.
.- Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics.
.- A Real-Analytic Approach to Differential-Algebraic Dynamic Logic.
.- SAT.
.- Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration.
.- Unfolding Boxes with Local Constraints.
Riassunto
This open access 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.
