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