CADE-30: 30TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

A
Abraham, Erika	Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method More is Less: Adding Polynomials for Faster Explanations in NLSAT FP A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination FP Projective Delineability for Single Cell Construction
Achammer, Fabian	Computing Witnesses Using the SCAN Algorithm
Ahmed, Tanbir	[FP] Symbolic Sets for Proving Bounds on Rado Numbers
Ahrens, Emma	Analyzing Weighted Abstract Reduction Systems via Semirings
B
Baader, Franz	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Baeta, Nuno	ADG-Lib Initiative A Generator of Geometry Deductive Database Method Provers
Baksys, Mantas	The TPTP Format for Tableaux Proofs
Barbosa, Haniel	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Barenbaum, Pablo	A Fresh Inductive Approach to Useful Call-by-Value
Barrett, Clark	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Bartl, Lukas	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Benzmüller, Christoph	Faithful Logic Embeddings in HOL – Deep and Shallow
Blaimschein, Katharina	Evaluating LLMs on Formal Models Coursework
Blanchette, Jasmin	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Borgwardt, Stefan	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Bourgeat, Thomas	Interoperability of Proof systems with SC-TPTP (System Description)
Boutry, Pierre	First-Order Simplification of GeoCoq using Dedukti An Automated Approach towards Constructivizing the GeoCoq Library On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
Briefs, Yasmine	From Building Blocks to Real SAT Solvers
Bright, Curtis	[FP] Symbolic Sets for Proving Bounds on Rado Numbers
Bromberger, Martin	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Brown, Chad	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Brown, Christopher	FP Projective Delineability for Single Cell Construction Presentation Only: Semantics of Division for Polynomial Solvers
C
Cabodi, Gianpiero	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Cailler, Julie	Interoperability of Proof systems with SC-TPTP (System Description) The ProoVer Competition at IJCAR 2026
Caires Ribeiro Santos, Ali Khan	Equational Reasoning Modulo Commutativity in Languages with Binders
Camurati, Paolo Enrico	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Chaabani, Mohamed	Verified Path Indexing
Cheese, Wine And	Action Planning == Wish List
Chvalovský, Karel	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Coghetto, Roland	IsaGeoCoq, a port of GeoCoq with Isabelle/HOL
Colin, Prunelle	On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
Coutelier, Robin	Term Ordering Diagrams
D
Dana-Picard, Thierry	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
Davenport, James H.	FP Projective Delineability for Single Cell Construction
De Bortoli, Filippo	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
de Moura, Leonardo	A Decade of Lean: Advancing Proof Automation for Mathematics and Software Verification
Desharnais, Martin	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
E
England, Matthew	FP Projective Delineability for Single Cell Construction
Erascu, Madalina	Opening, Christian Zipfel Award
F
Farzan, Azadeh	Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning
Felicissimo, Thiago	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Fernandez, Maribel	Equational Reasoning Modulo Commutativity in Languages with Binders
Fleury, Mathias	From Building Blocks to Real SAT Solvers
Frohn, Florian	Infinite State Model Checking by Learning Transitive Relations
Fuenmayor, David	StarExec-ARC
Fuhs, Carsten	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
G
Gambhir, Sankalp	Interoperability of Proof systems with SC-TPTP (System Description)
Gauthier, Thibault	Learning Conjecturing from Scratch
Gehring, Jannis	Premise Selection with the Alternating-Path-Method
Getachew, Estifanos	Relatively Complete and Efficient Partial Quantifier Elimination
Ghidini, Rebecca	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Giesl, Jürgen	Infinite State Model Checking by Learning Transitive Relations Analyzing Weighted Abstract Reduction Systems via Semirings
Graham-Lengrand, Stéphane	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. PO: Decision Heuristics in MCSat
Graziani, Pierluigi	Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey
Griggio, Alberto	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Guerdi, Massin	A Lambda-Superposition Tactic for Isabelle/HOL
Guilloud, Simon	Interoperability of Proof systems with SC-TPTP (System Description)
Guo, Liye	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Gurfinkel, Arie	Relatively Complete and Efficient Partial Quantifier Elimination
Géran, Yoan	First-Order Simplification of GeoCoq using Dedukti
Gévay, Gábor	Is a regular polygon determined by its diagonals?
H
Hader, Thomas	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. PO: Decision Heuristics in MCSat
Hajdu, Marton	Partial Redundancy in Saturation Term Ordering Diagrams
Heisinger, Simone	Evaluating LLMs on Formal Models Coursework
Hellwig, Jonathan	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Herklotz, Yann	Interoperability of Proof systems with SC-TPTP (System Description)
Herrmann, Roland	What's Decidable About Arrays With Sums?
Hetzl, Stefan	Computing Witnesses Using the SCAN Algorithm
Heule, Marijn	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification Unfolding Boxes with Local Constraints
Hirokawa, Nao	Lexicographic Combination of Reduction Pairs
Hofstadler, Clemens	EA Recycling Algebraic Proof Certificates
Holden, Sean	The TPTP Format for Clausal Connection Tableau Proofs The TPTP Format for Tableaux Proofs
Hoofd, Nick	Reinforcing students’ proof structure with Waterproof: an analysis
Hubauer, Thomas	Ontologies in Industry - The Good, the Bad, and the Ugly​
Hustadt, Ullrich	Modal Logic Reasoning: The Long View
I
Indrzejczak, Andrzej	Cut Elimination for Negative Free Logics with Definite Descriptions
Irfan, Ahmed	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. PO: Decision Heuristics in MCSat
J
Janicic, Predrag	Geometry Machine Revisited ADG-Lib Initiative
Janota, Mikoláš	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Janota, Mikoláš	Opening, Christian Zipfel Award
Jean, Alexandre	An Automated Approach towards Constructivizing the GeoCoq Library
Jouannaud, Jean-Pierre	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
K
Kassing, Jan-Christoph	Analyzing Weighted Abstract Reduction Systems via Semirings
Katoen, Joost-Pieter	Analyzing Weighted Abstract Reduction Systems via Semirings
Katzenberger, Michael	Manifold-based Proving Methods in Projective Geometry
Kaufmann, Daniela	EA Recycling Algebraic Proof Certificates
Kerekes, András	Towards automatic detection of geometric difficulty of geometry problems
Kesner, Delia	A Fresh Inductive Approach to Useful Call-by-Value
Keyser, John	Inference Maximizing Point Configurations for Parsimonious Algorithms
Khan, Harun	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Koopmann, Patrick	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Kop, Cynthia	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Kovács, Benedek	Is a regular polygon determined by its diagonals?
Kovács, Laura	Partial Redundancy in Saturation Term Ordering Diagrams
Kovács, Zoltán	Towards automatic detection of geometric difficulty of geometry problems Is a regular polygon determined by its diagonals? ADG-Lib Initiative Proving theorems on regular polygons by elimination --- the elementary way
Kreitz, Christoph	The Development of Interactive Theorem Proving
Kuncak, Viktor	Interoperability of Proof systems with SC-TPTP (System Description)
L
Leidinger, Hendrik	Computing Ground Congruence Classes
Lin, Zhengyao	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Lipparini, Enrico	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Lucas, Salvador	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Lund, Simon Tobias	Formalizing Axiomatics for First-Order Logic
M
Magaud, Nicolas	An Automated Approach towards Constructivizing the GeoCoq Library
Mansutti, Alessio	PO Integer Linear-Exponential Programming
Marinkovic, Vesna	Different Types of Locus Dependencies in Solving Geometry Construction Problems
Marinković, Vesna	Automating Geometry Construction Problems
Marić, Filip	ADG-Lib Initiative Different Types of Locus Dependencies in Solving Geometry Construction Problems
Mascarenhas, Tomaz	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Mathonet, Pierre	FP Projective Delineability for Single Cell Construction
Merz, Stephan	Invariant Synthesis: Decidable Fragments to the Rescue
Michel, Lucas	FP Projective Delineability for Single Cell Construction
Middeldorp, Aart	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Milicich, Mariana	A Fresh Inductive Approach to Useful Call-by-Value
Mohamed, Abdalrhman	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
N
Nalbach, Jasper	More is Less: Adding Polynomials for Faster Explanations in NLSAT FP A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination FP Projective Delineability for Single Cell Construction
Nalon, Cláudia	From Modal Sequent Calculi to Modal Resolution
Nantes Sobrinho, Daniele	Equational Reasoning Modulo Commutativity in Languages with Binders
Narboux, Julien	Geometry Machine Revisited ADG-Lib Initiative
Niederhauser, Johannes	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Nipkow, Tobias	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
O
Olšák, Miroslav	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Otop, Jan	Anti-pattern templates
P
Palena, Marco	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Parno, Bryan	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Pasini, Paolo	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Pattinson, Dirk	From Modal Sequent Calculi to Modal Resolution
Pereira-Albert, Álvaro	Computing loci with GeoGebra Discovery: some issues and suggestions
Peruri, Sourabh	From Modal Sequent Calculi to Modal Resolution
Petiurenko, Anna	ADG-Lib Initiative
Petkovic Komel, Anja	Vampire and Dedukti Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Plaisted, David	Planning with Equality
Platzer, André	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Poiroux, Auguste	Interoperability of Proof systems with SC-TPTP (System Description)
Portegies, Jim	Reinforcing students’ proof structure with Waterproof: an analysis
Promies, Valentin	Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method More is Less: Adding Polynomials for Faster Explanations in NLSAT
Przybocki, Benjamin	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
Q
Qian, Long	Unfolding Boxes with Local Constraints
Quaresma, Pedro	ADG-Lib Initiative A Generator of Geometry Deductive Database Method Provers Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey
R
Ratschan, Stefan	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Rawson, Michael	Higher-order Verification of Skolemization Steps Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Recio, Tomas	Computing loci with GeoGebra Discovery: some issues and suggestions
Reynolds, Andrew	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Richter-Gebert, Jürgen	Manifold-based Proving Methods in Projective Geometry
Robillard, Simon	Verified Path Indexing Teaching Automated Deduction: an Implementation-BasedApproach with Maude
Roveri, Marco	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Rümmer, Philipp	What's Decidable About Arrays With Sums?
S
Saito, Teppei	Lexicographic Combination of Reduction Pairs
Schlichtkrull, Anders	Formalizing Axiomatics for First-Order Logic
Schmidt, Renate A.	Computing Witnesses Using the SCAN Algorithm Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract) Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Schoisswohl, Johannes	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Schulz, Stephan	Premise Selection with the Alternating-Path-Method Planning with Equality
Schüler-Meyer, Alexander	Reinforcing students’ proof structure with Waterproof: an analysis
Sebastiani, Roberto	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Seidl, Martina	Evaluating LLMs on Formal Models Coursework
Shah, Amar	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Sharma, Shivam	Inference Maximizing Point Configurations for Parsimonious Algorithms
Shoham, Sharon	Taming Infinity for Verification in First-Order Logic
Sidhoum, Romain	Teaching Automated Deduction: an Implementation-BasedApproach with Maude
Sindoni, Giulia	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Sofronie-Stokkermans, Viorica	On Symbol Elimination and Uniform Interpolation in Theory Extensions
Steen, Alex	The TPTP Format for Interpretations
Stevens, Lukas	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Subercaseaux, Bernardo	Unfolding Boxes with Local Constraints
Suda, Martin	Equisatisfiable Inferences Boosting Vampire with Neural Networks Efficient Neural Clause-Selection Reinforcement
Sukilovic, Tijana	Different Types of Locus Dependencies in Solving Geometry Construction Problems
Sutcliffe, Geoff	Welcome Review of the TPTP format for derivations Proof Verification with GDV and GDV-LP The TPTP Format for Tableaux Proofs
Szeider, Stefan	Mathematical Discovery with SAT Modulo Symmetries
T
Taprogge, Melanie	Leo-III and LambdaPi Towards the Verification of Higher-Order Logic Automated Reasoning
Tinelli, Cesare	PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability
Toledo, Guilherme	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
Tonetta, Stefano	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Tourret, Sophie	Conflict-based Literal Model Generation
Trefler, Richard	Relatively Complete and Efficient Partial Quantifier Elimination
U
Urban, Josef	Learning Conjecturing from Scratch
V
Velez, M. Pilar	Computing loci with GeoGebra Discovery: some issues and suggestions
Villadsen, Jørgen	Teaching Axiomatic Systems and Metatheory in Isabelle Formalizing Axiomatics for First-Order Logic
Voronkov, Andrei	Partial Redundancy in Saturation Term Ordering Diagrams Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
W
Wagner, Paul	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Wang, Eric	Unfolding Boxes with Local Constraints
Weidenbach, Christoph	TBA Computing Ground Congruence Classes A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Wemmenhove, Jelle	Reinforcing students’ proof structure with Waterproof: an analysis
Wernhard, Christoph	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Y
Yin, Hongkai	Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
Z
Zaman, Lamina	[FP] Symbolic Sets for Proving Bounds on Rado Numbers
Zenaïdi, Naïm	FP Projective Delineability for Single Cell Construction
Zhao, Yizheng	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Zhou, Yi	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Zohar, Yoni	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
Zombori, Zsolt	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures

Disclaimer | Powered by EasyChair Smart Program