CADE-30: 30TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

A
Abraham, Erika	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Achammer, Fabian	Computing Witnesses Using the SCAN Algorithm
Ahrens, Emma	Analyzing Weighted Abstract Reduction Systems via Semirings
B
Baader, Franz	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Barenbaum, Pablo	A Fresh Inductive Approach to Useful Call-by-Value
Bartl, Lukas	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Benzmüller, Christoph	Faithful Logic Embeddings in HOL – Deep and Shallow
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)
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
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)
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
Chvalovský, Karel	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Coutelier, Robin	Term Ordering Diagrams
D
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
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
Frohn, Florian	Infinite State Model Checking by Learning Transitive Relations
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.
Griggio, Alberto	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
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
H
Hader, Thomas	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Hajdu, Marton	Partial Redundancy in Saturation Term Ordering Diagrams
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
Hubauer, Thomas	TBA
Hustadt, Ullrich	TBA
I
Indrzejczak, Andrzej	Cut Elimination for Negative Free Logics with Definite Descriptions
Irfan, Ahmed	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
J
Janota, Mikoláš	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
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
Kesner, Delia	A Fresh Inductive Approach to Useful Call-by-Value
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, Laura	Partial Redundancy in Saturation Term Ordering Diagrams
Kreitz, Christoph	TBA
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
M
Middeldorp, Aart	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Milicich, Mariana	A Fresh Inductive Approach to Useful Call-by-Value
N
Nalbach, Jasper	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Nalon, Cláudia	From Modal Sequent Calculi to Modal Resolution
Nantes Sobrinho, Daniele	Equational Reasoning Modulo Commutativity in Languages with Binders
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
Peruri, Sourabh	From Modal Sequent Calculi to Modal Resolution
Petković Komel, Anja	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Platzer, André	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Poiroux, Auguste	Interoperability of Proof systems with SC-TPTP (System Description)
Promies, Valentin	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Przybocki, Benjamin	Being polite is not enough (and other limits of theory combination)
Q
Qian, Long	Unfolding Boxes with Local Constraints
R
Ratschan, Stefan	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Rawson, Michael	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Robillard, Simon	Verified Path Indexing
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
Schmidt, Renate A.	Computing Witnesses Using the SCAN Algorithm 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
Sebastiani, Roberto	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Shah, Amar	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Shoham, Sharon	Taming Infinity for Verification in First-Order Logic
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
Stevens, Lukas	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Subercaseaux, Bernardo	Unfolding Boxes with Local Constraints
Suda, Martin	Efficient Neural Clause-Selection Reinforcement
Sutcliffe, Geoff	Welcome Review of the TPTP format for derivations
T
Taprogge, Melanie	Towards the Verification of Higher-Order Logic Automated Reasoning
Toledo, Guilherme	Being polite is not enough (and other limits of theory combination)
Tonetta, Stefano	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Trefler, Richard	Relatively Complete and Efficient Partial Quantifier Elimination
U
Urban, Josef	Learning Conjecturing from Scratch
V
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	Computing Ground Congruence Classes A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Wernhard, Christoph	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Z
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)
Zombori, Zsolt	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures

Disclaimer | Powered by EasyChair Smart Program