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