Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings

Description

This book constitutes the proceeding of the 27th International Conference on Automated Deduction, CADE 27, held in Natal, Brazil, in August 2019. The 27 full papers and 7 system descriptions presented were carefully reviewed and selected from 65 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. Front Matter ....Pages i-xxiii Unification Modulo Lists with Reverse Relation with Certain Word Equations (Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michael Rusinowitch)....Pages 1-17 On the Width of Regular Classes of Finite Structures (Alexsander Andrade de Melo, Mateus de Oliveira Oliveira)....Pages 18-34 Extending SMT Solvers to Higher-Order Logic (Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark Barrett)....Pages 35-54 Superposition with Lambdas (Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann)....Pages 55-73 Restricted Combinatory Unification (Ahmed Bhayat, Giles Reger)....Pages 74-93 \(\mathsf {dL}_{\iota }\): Definite Descriptions in Differential Dynamic Logic (Brandon Bohrer, Manuel Fernández, André Platzer)....Pages 94-110 SPASS-SATT (Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach)....Pages 111-122 GRUNGE: A Grand Unified ATP Challenge (Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban)....Pages 123-141 Model Completeness, Covers and Superposition (Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin)....Pages 142-160 A Tableaux Calculus for Default Intuitionistic Logic (Valentin Cassano, Raul Fervari, Guillaume Hoffmann, Carlos Areces, Pablo F. Castro)....Pages 161-177 NIL: Learning Nonlinear Interpolants (Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan)....Pages 178-196 ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E (Karel Chvalovský, Jan Jakubův, Martin Suda, Josef Urban)....Pages 197-215 Towards Physical Hybrid Systems (Katherine Cordwell, André Platzer)....Pages 216-232 SCL Clause Learning from Simple Models (Alberto Fiori, Christoph Weidenbach)....Pages 233-249 Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection (Ulrich Furbach, Teresa Krämer, Claudia Schon)....Pages 250-268 Computing Expected Runtimes for Constant Probability Programs (Jürgen Giesl, Peter Giesl, Marcel Hark)....Pages 269-286 Automatic Generation of Logical Models with AGES (Raúl Gutiérrez, Salvador Lucas)....Pages 287-299 Automata Terms in a Lazy WSkS Decision Procedure (Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Tomáš Vojnar)....Pages 300-318 Confluence by Critical Pair Analysis Revisited (Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi)....Pages 319-336 Composing Proof Terms (Christina Kohl, Aart Middeldorp)....Pages 337-353 Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (Di Long Li, Alwen Tiu)....Pages 354-365 Towards Bit-Width-Independent Proofs in SMT Solvers (Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli)....Pages 366-384 On Invariant Synthesis for Parametric Systems (Dennis Peuter, Viorica Sofronie-Stokkermans)....Pages 385-405 The Aspect Calculus (David A. Plaisted)....Pages 406-424 Uniform Substitution at One Fell Swoop (André Platzer)....Pages 425-441 A Formally Verified Abstract Account of Gödel’s Incompleteness Theorems (Andrei Popescu, Dmitriy Traytel)....Pages 442-461 Old or Heavy? Decaying Gracefully with Age/Weight Shapes (Michael Rawson, Giles Reger)....Pages 462-476 Induction in Saturation-Based Proof Search (Giles Reger, Andrei Voronkov)....Pages 477-494 Faster, Higher, Stronger: E 2.3 (Stephan Schulz, Simon Cruanes, Petar Vukmirović)....Pages 495-507 Certified Equational Reasoning via Ordered Completion (Christian Sternagel, Sarah Winkler)....Pages 508-525 JGXYZ: An ATP System for Gap and Glut Logics (Geoff Sutcliffe, Francis Jeffry Pelletier)....Pages 526-537 GKC: A Reasoning System for Large Knowledge Bases (Tanel Tammet)....Pages 538-549 Optimization Modulo the Theory of Floating-Point Numbers (Patrick Trentin, Roberto Sebastiani)....Pages 550-567 FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions (Yizheng Zhao, Renate A. Schmidt)....Pages 568-579 Back Matter ....Pages 581-582