| Invited Talk / Session 1： |
| SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke |
| Session 2 |
| Equational Abstractions / José Meseguer ; Miguel Palomino ; Narciso Martí-Oliet |
| Deciding Inductive Validity of Equations / Jürgen Giesl ; Deepak Kapur |
| Automating the Dependency Pair Method / Nao Hirokawa ; Aart Middeldorp |
| An AC-Compatible Knuth-Bendix Order / Konstantin Korovin ; Andrei Voronkov |
| Session 3 |
| The Complexity of Finite Model Reasoning in Description Logics / Carsten Lutz ; Ulrike Sattler ; Lidia Tendera |
| Optimizing a BDD-Based Modal Solver / Guoqiang Pan ; Moshe Y. Vardi |
| A Translation of Looping Alternating Automata into Description Logics / Jan Hladik |
| Session 4 |
| Foundational Certified Code in a Metalogical Framework / Karl Crary ; Susmit Sarkar |
| Proving Pointer Programs in Higher-Order Logic / Farhad Mehta ; Tobias Nipkow |
| λ / Dimitri Hendriks ; Vincent van Oostrom |
| Subset Types and Partial Functions / Aaron Stump |
| Session 5 |
| Reasoning about Quantifiers by Matching in the E-graphGreg Nelson |
| Session 6 |
| A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols / Sumit Gulwani ; George C. Necula |
| Superposition Modulo a Shostak Theory / Harald Ganzinger ; Thomas Hillenbrand ; Uwe Waldmann |
| Canonization for Disjoint Unions of Theories / Sava Krstić ; Sylvain Conchon |
| Matching in a Class of Combined Non-disjoint Theories / Christophe Ringeissen |
| Session 7 |
| Reasoning about Iteration in Gödel's Class Theory / Johan Gijsbertus Frederik Belinfante |
| Algorithms for Ordinal Arithmetic / Panagiotis Manolios ; Daron Vroon |
| Certifying Solutions to Permutation Group Problems / Arjeh Cohen ; Scott H. Murray ; Martin Pollet ; Volker Sorge |
| System Descriptions / Session 8： |
| TRP++ 2.0: A Temporal Resolution Prover / Ullrich Hustadt ; Boris Konev |
| IsaPlanner: A Prototype Proof Planner in Isabelle / Lucas Dixon ; Jacques Fleuriot |
| 'Living Book': - 'Deduction', 'Slicing', 'Interaction' / Peter Baumgartner ; Ulrich Furbach ; Margret Gross-Hardt ; Alex Sinner |
| The Homer System / Simon Colton ; Sophie Huczynska |
| CASC-19 Results / Session 9： |
| The CADE-19 ATP System Competition / Geoff Sutcliffe ; Christian Suttner |
| Proof Search and Proof Check for Equational and Inductive Theorems / Eric Deplagne ; Claude Kirchner ; Hélène Kirchner ; Quang Huy NguyenSession 10： |
| The New Waldmeister Loop at Work / Jean-Marie Gaillourdet ; Bernd Löuchner ; Hendrik SpiesSession 11： |
| About VeriFun / Christoph Walther ; Stephan Schweitzer |
| How to Prove Inductive Theorems? QuodLibet! / Jürgen Avenhaus ; Ulrich Kühler ; Tobias Schmidt-Samoa ; Claus-Peter Wirth |
| Reasoning about Qualitative Representations of Space and Time / Anthony G. CohnSession 12： |
| Session 13 |
| Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation / Jürgen Stuber |
| The Model Evolution Calculus / Cesare Tinelli |
| Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms / Hans de Nivelle |
| Efficient Instance Retrieval with Standard and Relational Path Indexing / Alexandre Riazanov |
| Session 14 |
| Monodic Temporal Resolution / Anatoly Degtyarev ; Michael Fisher |
| A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae / Renate A. Schmidt |
| Schematic Saturation for Decision and Unification Problems / Christopher Lynch |
| Session 15 |
| Unification Modulo ACUI Plus Homomorphisms/Distributivity / Siva Anantharaman ; Paliath Narendran ; Michael Rusinowitch |
| Source-Tracking Unification / Venkatesh Choppella ; Christopher T. Haynes |
| Optimizing Higher-Order Pattern Unification / Brigitte Pientka ; Frank Pfenning |
| Decidability of Arity-Bounded Higher-Order Matching / Manfred Schmidt-Schauß |
| Author Index |
| Invited Talk / Session 1： |
| SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke |
| Session 2 |
ＥＢ
