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 |
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 |