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