CADE-27: 27TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

A
An, Jie	NIL: Learning Nonlinear Interpolants
Anantharaman, Siva	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Andrade de Melo, Alexsander	On the Width of Regular Classes of Finite Structures
Areces, Carlos	A Tableaux Calculus for Default Intuitionistic Logic
B
Barbosa, Haniel	Extending SMT solvers to Higher-Order Logic
Barrett, Clark	Extending SMT solvers to Higher-Order Logic Towards Bit Width Independent Proofs in SMT Solvers
Bentkamp, Alexander	Superposition with Lambdas
Bhayat, Ahmed	Restricted Combinatory Unification
Blanchette, Jasmin Christian	Superposition with Lambdas
Bohrer, Brandon	dLi: Definite Descriptions in Differential Dynamic Logic
Bromberger, Martin	SPASS-SATT a CDCL(LA) Solver (System Description)
Brown, Chad	GRUNGE: The Grand Unified ATP Challenge
C
Calvanese, Diego	Model Completeness, Covers and Superposition
Cassano, Valentin	A Tableaux Calculus for Default Intuitionistic Logic
Castro, Pablo	A Tableaux Calculus for Default Intuitionistic Logic
Chen, Mingshuai	NIL: Learning Nonlinear Interpolants
Chvalovský, Karel	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Cordwell, Katherine	Towards Physical Hybrid Systems
Cremers, Cas	Invited Talk: Automated Reasoning for Security Protocols
Cruanes, Simon	Faster, Higher, Stronger: E 2.3 (System Description)
D
De Oliveira Oliveira, Mateus	On the Width of Regular Classes of Finite Structures
E
El Ouraoui, Daniel	Extending SMT solvers to Higher-Order Logic
F
Fernandez, Manuel	dLi: Definite Descriptions in Differential Dynamic Logic
Fervari, Raul	A Tableaux Calculus for Default Intuitionistic Logic
Fiori, Alberto	SCL -- Clause Learning from Simple Models
Fleury, Mathias	SPASS-SATT a CDCL(LA) Solver (System Description)
Furbach, Ulrich	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
G
Gauthier, Thibault	GRUNGE: The Grand Unified ATP Challenge
Ghilardi, Silvio	Model Completeness, Covers and Superposition
Gianola, Alessandro	Model Completeness, Covers and Superposition
Giesl, Jürgen	Computing Expected Runtimes for Constant Probability Programs
Giesl, Peter	Computing Expected Runtimes for Constant Probability Programs
Gutiérrez, Raúl	Automatic Generation of Logical Models with AGES (System Description)
H
Hark, Marcel	Computing Expected Runtimes for Constant Probability Programs
Havlena, Vojtěch	Automata Terms in a Lazy WSkS Decision Procedure
Hibbs, Peter	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Hirokawa, Nao	Confluence by Critical Pair Analysis Revisited
Hoffmann, Guillaume	A Tableaux Calculus for Default Intuitionistic Logic
Holik, Lukas	Automata Terms in a Lazy WSkS Decision Procedure
J
Jakubuv, Jan	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
K
Kaliszyk, Cezary	GRUNGE: The Grand Unified ATP Challenge
Kapur, Deepak	NIL: Learning Nonlinear Interpolants
Kohl, Christina	Composing Proof Terms
Krämer, Teresa	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
L
Lengal, Ondrej	Automata Terms in a Lazy WSkS Decision Procedure
Li, Di Long	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
Lucas, Salvador	Automatic Generation of Logical Models with AGES (System Description)
M
Mahboubi, Assia	Invited Talk: Computer Deduction and (Formal) Proofs in Mathematics
Middeldorp, Aart	Composing Proof Terms
Montali, Marco	Model Completeness, Covers and Superposition
N
Nagele, Julian	Confluence by Critical Pair Analysis Revisited
Narendran, Paliath	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Niemetz, Aina	Towards Bit Width Independent Proofs in SMT Solvers
O
Oyamaguchi, Michio	Confluence by Critical Pair Analysis Revisited
P
Pelletier, Francis Jeffry	JGXYZ - An ATP System for Gap and Glut Logics (System Description)
Peuter, Dennis	On Invariant Synthesis for Parametric Systems
Plaisted, David	The Aspect Calculus
Platzer, André	Uniform Substitution in One Fell Swoop dLi: Definite Descriptions in Differential Dynamic Logic Towards Physical Hybrid Systems
Popescu, Andrei	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
Preiner, Mathias	Towards Bit Width Independent Proofs in SMT Solvers
R
Rawson, Michael	Old or Heavy? Decaying Gracefully with Age/Weight Shapes.
Reger, Giles	Old or Heavy? Decaying Gracefully with Age/Weight Shapes. Induction in Saturation-Based Proof Search Restricted Combinatory Unification
Reynolds, Andrew	Extending SMT solvers to Higher-Order Logic Towards Bit Width Independent Proofs in SMT Solvers
Rivkin, Andrey	Model Completeness, Covers and Superposition
Rusinowitch, Michael	Unification modulo Lists with Reverse - Relation with Certain Word Equations
S
Schmidt, Renate A.	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
Schon, Claudia	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
Schulz, Stephan	Faster, Higher, Stronger: E 2.3 (System Description)
Schwarz, Simon	SPASS-SATT a CDCL(LA) Solver (System Description)
Sebastiani, Roberto	Optimization Modulo the Theory of Floating-Point Numbers
Sofronie-Stokkermans, Viorica	On Invariant Synthesis for Parametric Systems
Sternagel, Christian	Certified Equational Reasoning via Ordered Completion
Suda, Martin	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Sutcliffe, Geoff	The CADE-27 ATP System Competition - CASC-27 GRUNGE: The Grand Unified ATP Challenge JGXYZ - An ATP System for Gap and Glut Logics (System Description)
T
Tammet, Tanel	GKC: a Reasoning System for Large Knowledge Bases (System Description)
Tinelli, Cesare	Invited Talk: From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT Extending SMT solvers to Higher-Order Logic Towards Bit Width Independent Proofs in SMT Solvers
Tiu, Alwen	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
Tourret, Sophie	Superposition with Lambdas
Traytel, Dmitriy	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
Trentin, Patrick	Optimization Modulo the Theory of Floating-Point Numbers
U
Urban, Josef	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E GRUNGE: The Grand Unified ATP Challenge
V
van Oostrom, Vincent	Confluence by Critical Pair Analysis Revisited
Vojnar, Tomas	Automata Terms in a Lazy WSkS Decision Procedure
Voronkov, Andrei	Induction in Saturation-Based Proof Search
Vukmirović, Petar	Superposition with Lambdas Faster, Higher, Stronger: E 2.3 (System Description)
W
Waldmann, Uwe	Superposition with Lambdas
Wang, Jian	NIL: Learning Nonlinear Interpolants
Weidenbach, Christoph	SCL -- Clause Learning from Simple Models SPASS-SATT a CDCL(LA) Solver (System Description)
Winkler, Sarah	Certified Equational Reasoning via Ordered Completion
Z
Zhan, Bohua	NIL: Learning Nonlinear Interpolants
Zhan, Naijun	NIL: Learning Nonlinear Interpolants
Zhao, Yizheng	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
Zohar, Yoni	Towards Bit Width Independent Proofs in SMT Solvers

Disclaimer | Powered by EasyChair Smart Program