CADE-26 Accepted Papers
Transfinite Knuth-Bendix Orders for Lambda-Free Higher-Order Terms
The binomial pricing model in finance: a formalization in Isabelle
Theorem Proving for Metric Temporal Logic over the Naturals
Satisfiability Modulo Bounded Checking
An Efficient Proof-Producing Framework for Formula Processing
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Biabduction (and Related Problems) in Array Separation Logic
Short Proofs without New Variables
A Unifying Principle for Clause Elimination in First-Order Logic
CSI: New Evidence - A Progress Report
Efficient Certified RAT Verification
Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
Translating between implicit and explicit versions of proof
Notions of Knowledge in Combinations of Theories Sharing Constructors
A Decision Procedure for Restricted Intensional Sets
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
WorkflowFM: A logic-based formal verification framework for process specification and composition
Efficient Verified (UN)SAT Certificate Checking
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
Detecting Inconsistencies in Large First-Order Knowledge Bases
Satisfiability Modulo Transcendental Functions via Incremental Linearization
Monte Carlo Tableau Proof Search
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Certifying Safety and Termination Proofs for Integer Transition Systems
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Linear Integer Arithmetic
Decision Procedures for Theories of Sets with Measures
Splitting Proofs for Interpolation
Relational Constraint Solving in SMT
Satisfiability Modulo Theories and Assignments