CADE-29: 29TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

B
Barrett, Clark	Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Benzmüller, Christoph	Theorem Proving in Dependently-Typed Higher-Order Logic
Berg, Jeremias	Certified Core-Guided MaxSAT Solving
Bhayat, Ahmed	Superposition with Delayed Unification
Bjorner, Nikolaj	On Incremental Pre-processing for SMT
Blanchette, Jasmin	Lambda-Superposition: From Theory to Trophy Verified Given Clause Procedures
Bogaerts, Bart	Certified Core-Guided MaxSAT Solving
Boigelot, Bernard	Decidability of difference logic over the reals with uninterpreted unary predicates
Bonacina, Maria Paola	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Brieger, Marvin	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Bromberger, Martin	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Bruse, Florian	Formal Reasoning about Influence in Natural Sciences Experiments
C
Chen, Yu-Fang	A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
Coutelier, Robin	SAT-Based Subsumption Resolution
D
Desharnais, Martin	An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Dixon, Clare	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Draheim, Dirk	An Experimental Pipeline for Automated Reasoning in Natural Language
F
Fan, Yuheng	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Fazekas, Katalin	On Incremental Pre-processing for SMT
Fernandez, Maribel	Nominal Techniques for Software Specification and Verification
Fiedor, Tomas	Reasoning about Regular Properties: A Comparative Study
Fleury, Mathias	A more Pragmatic CDCL for IsaSAT and targetting LLVM
Fontaine, Pascal	Decidability of difference logic over the reals with uninterpreted unary predicates
Frohn, Florian	Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper
G
Giesl, Jürgen	Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs Proving Termination of C Programs with Lists
Graham-Lengrand, Stéphane	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Görlitz, Oliver	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
H
Hausmann, Daniel	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Henkel, Elisabeth	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Hensel, Jera	Proving Termination of C Programs with Lists
Hirokawa, Nao	Left-Linear Completion with AC Axioms
Hoenicke, Jochen	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Holík, Lukáš	Reasoning about Regular Properties: A Comparative Study
Hozzová, Petra	Program Synthesis in Saturation
Hruska, Martin	Reasoning about Regular Properties: A Comparative Study
Humml, Merlin	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Hustadt, Ullrich	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
I
Indrzejczak, Andrzej	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
J
Jain, Chaahat	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Jamnik, Mateja	How Can We Make Trustworthy AI?
Järv, Priit	An Experimental Pipeline for Automated Reasoning in Natural Language
K
Kassing, Jan-Christoph	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Kovács, Laura	Program Synthesis in Saturation SAT-Based Subsumption Resolution
Kreuzer, Katharina	Verification of NP-hardness for Exact Lattice Problems
L
Lammich, Peter	A more Pragmatic CDCL for IsaSAT and targetting LLVM
Lange, Martin	Formal Reasoning about Influence in Natural Sciences Experiments
M
Middeldorp, Aart	Confluence Criteria for Logically Constrained Rewrite Systems Left-Linear Completion with AC Axioms
Mitsch, Stefan	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Möller, Sören	Formal Reasoning about Influence in Natural Sciences Experiments
N
Nalon, Cláudia	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Nantes-Sobrinho, Daniele	Towards Fast Nominal Anti-Unification of Letrec-Expressions
Niederhauser, Johannes	Left-Linear Completion with AC Axioms
Nigam, Vivek	Incremental Rewriting Modulo SMT
Nipkow, Tobias	Verification of NP-hardness for Exact Lattice Problems
Nordström, Jakob	Certified Core-Guided MaxSAT Solving
Norman, Chase	Program Synthesis in Saturation
O
Oertel, Andy	Certified Core-Guided MaxSAT Solving
P
Papacchini, Fabio	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Pattinson, Dirk	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Petrukhin, Yaroslav	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Peuter, Dennis	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Platzer, André	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Prucker, Simon	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Q
Qiu, Qi	Verified Given Clause Procedures
R
Rabe, Florian	Theorem Proving in Dependently-Typed Higher-Order Logic
Rath, Jakob	SAT-Based Subsumption Resolution
Rawson, Michael	Superposition with Delayed Unification SAT-Based Subsumption Resolution
Rogalewicz, Adam	Reasoning about Regular Properties: A Comparative Study
Rothgang, Colin	Theorem Proving in Dependently-Typed Higher-Order Logic
Rümmer, Philipp	A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
S
Schindler, Tanja	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Schmidt-Schauss, Manfred	Towards Fast Nominal Anti-Unification of Letrec-Expressions
Schoisswohl, Johannes	Superposition with Delayed Unification
Schröder, Lutz	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Schöpf, Jonas	Confluence Criteria for Logically Constrained Rewrite Systems
Sofronie-Stokkermans, Viorica	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Stevens, Lukas	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Síč, Juraj	Reasoning about Regular Properties: A Comparative Study
T
Talcott, Carolyn	Incremental Rewriting Modulo SMT
Tammet, Tanel	An Experimental Pipeline for Automated Reasoning in Natural Language
Thunert, Sebastian	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Toledo, Guilherme	Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Tourret, Sophie	Verified Given Clause Procedures
Tsai, Wei-Lun	A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
V
Vandesande, Dieter	Certified Core-Guided MaxSAT Solving
Vardi, Moshe	Automated Reasoning with Data
Vargovčík, Pavol	Reasoning about Regular Properties: A Comparative Study
Vauthier, Christophe	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Vergain, Baptiste	Decidability of difference logic over the reals with uninterpreted unary predicates
Verrev, Martin	An Experimental Pipeline for Automated Reasoning in Natural Language
Voronkov, Andrei	Program Synthesis in Saturation
W
Weidenbach, Christoph	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Whitters, Gerald	Incremental Rewriting Modulo SMT
X
Xiong, Weiqiang	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Xu, Runqing	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Z
Zhan, Bohua	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Zohar, Yoni	Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness

Disclaimer | Powered by EasyChair Smart Program