On the Width of Regular Classes of Finite Structures

Alexsander Andrade de Melo and Mateus De Oliveira Oliveira

Names are not just Sound and Smoke: Word Embeddings for Axiom Selection

Ulrich Furbach, Teresa Krämer and Claudia Schon

GKC: a Reasoning System for Large Knowledge Bases (System Description)

Tanel Tammet

Towards Physical Hybrid Systems

Katherine Cordwell and André Platzer

dLi: Definite Descriptions in Differential Dynamic Logic

Brandon Bohrer, Manuel Fernandez and André Platzer

Invited Talk: From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT

Andrew Reynolds and Cesare Tinelli

Model Completeness, Covers and Superposition

Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali and Andrey Rivkin

Invited Talk: Computer Deduction and (Formal) Proofs in Mathematics

Assia Mahboubi

Extending SMT solvers to Higher-Order Logic

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett

Uniform Substitution in One Fell Swoop

André Platzer

Automata Terms in a Lazy WSkS Decision Procedure

Vojtěch Havlena, Lukas Holik, Ondrej Lengal and Tomas Vojnar

Computing Expected Runtimes for Constant Probability Programs

Jürgen Giesl, Peter Giesl and Marcel Hark

GRUNGE: A Grand Unified ATP Challenge

Chad Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe and Josef Urban

SCL -- Clause Learning from Simple Models

Alberto Fiori and Christoph Weidenbach

Invited Talk: Automated Reasoning for Security Protocols

Cas Cremers

Faster, Higher, Stronger: E 2.3 (System Description)

Stephan Schulz, Simon Cruanes and Petar Vukmirović

SPASS-SATT a CDCL(LA) Solver (System Description)

Martin Bromberger, Mathias Fleury, Simon Schwarz and Christoph Weidenbach

Composing Proof Terms

Christina Kohl and Aart Middeldorp

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Karel Chvalovský, Jan Jakubuv, Martin Suda and Josef Urban

Certified Equational Reasoning via Ordered Completion

Christian Sternagel and Sarah Winkler

Automatic Generation of Logical Models with AGES

Raúl Gutiérrez and Salvador Lucas

Towards Bit Width Independent Proofs in SMT Solvers

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett and Cesare Tinelli

Superposition with Lambdas

Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović and Uwe Waldmann

Restricted Combinatory Unification

Ahmed Bhayat and Giles Reger

Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)

Di Long Li and Alwen Tiu

On Invariant Synthesis for Parametric Systems

Dennis Peuter and Viorica Sofronie-Stokkermans

Optimization Modulo the Theory of Floating-Point Numbers

Patrick Trentin and Roberto Sebastiani

Old or Heavy? Decaying Gracefully with Age/Weight Shapes.

Michael Rawson and Giles Reger

NIL: Learning Nonlinear Interpolants

Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur and Naijun Zhan

Confluence by Critical Pair Analysis Revisited

Nao Hirokawa, Julian Nagele, Vincent Van Oostrom and Michio Oyamaguchi

A Tableaux Calculus for Default Intuitionistic Logic

Valentin Cassano, Raul Fervari, Guillaume Hoffmann, Carlos Areces and Pablo Castro

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems

Andrei Popescu and Dmitriy Traytel

Unification modulo Lists with Reverse - Relation with Certain Word Equations

Siva Anantharaman, Peter Hibbs, Paliath Narendran and Michael Rusinowitch

The Aspect Calculus

David Plaisted