Program / Accepted papers

The proceedings (LNAI 11716) are available on Springer’s site.

The program is available here.

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)


  • 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).