Front matter
1
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking
Edmund M. Clarke
2-16
Equational Abstractions
José Meseguer, Miguel Palomino and Narciso Martí-Oliet
17-31
Deciding Inductive Validity of Equations
Jürgen Giesl and Deepak Kapur
32-46
Automating the Dependency Pair Method
Nao Hirokawa and Aart Middeldorp
47-59
An AC-Compatible Knuth-Bendix Order
Konstantin Korovin and Andrei Voronkov
60-74
The Complexity of Finite Model Reasoning in Description Logics
Carsten Lutz, Ulrike Sattler and Lidia Tendera
75-89
Optimizing a BDD-Based Modal Solver
Guoqiang Pan and Moshe Y. Vardi
90-105
A Translation of Looping Alternating Automata into Description Logics
Jan Hladik and Ulrike Sattler
106-120
Foundational Certified Code in a Metalogical Framework
Karl Crary and Susmit Sarkar
121-135
Proving Pointer Programs in Higher-Order Logic
Farhad Mehta and Tobias Nipkow
136-150
⋌
Dimitri Hendriks and Vincent van Oostrom
151-165
Subset Types and Partial Functions
Aaron Stump
166
Reasoning about Quantifiers by Matching in the E-graph
Greg Nelson
167-181
A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols
Sumit Gulwani and George C. Necula
182-196
Superposition Modulo a Shostak Theory
Harald Ganzinger, Thomas Hillenbrand and Uwe Waldmann
197-211
Canonization for Disjoint Unions of Theories
Sava Krstić and Sylvain Conchon
212-227
Matching in a Class of Combined Non-disjoint Theories
Christophe Ringeissen
228-242
Reasoning about Iteration in Gödel’s Class Theory
Johan Gijsbertus Frederik Belinfante
243-257
Algorithms for Ordinal Arithmetic
Panagiotis Manolios and Daron Vroon
258-273
Certifying Solutions to Permutation Group Problems
Arjeh Cohen, Scott H. Murray, Martin Pollet and Volker Sorge
274-278
TRP++ 2.0: A Temporal Resolution Prover
Ullrich Hustadt and Boris Konev
279-283
IsaPlanner: A Prototype Proof Planner in Isabelle
Lucas Dixon and Jacques Fleuriot
284-288
’Living Book’ :- ’Deduction’, ’Slicing’, ’Interaction’
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt and Alex Sinner
289-294
The Homer System
Simon Colton and Sophie Huczynska
295-296
The CADE-19 ATP System Competition
Geoff Sutcliffe and Christian Suttner
297-316
Proof Search and Proof Check for Equational and Inductive Theorems
Eric Deplagne, Claude Kirchner, Hélène Kirchner and Quang Huy Nguyen
317-321
The New WALDMEISTER Loop at Work
Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner and Hendrik Spies
322-327
About VeriFun
Christoph Walther and Stephan Schweitzer
328-333
How to Prove Inductive Theorems? QuodLibet!
Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa and Claus-Peter Wirth
334
Reasoning about Qualitative Representations of Space and Time
Anthony G. Cohn
335-349
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
Harald Ganzinger and Jürgen Stuber
350-364
The Model Evolution Calculus
Peter Baumgartner and Cesare Tinelli
365-379
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
Hans de Nivelle
380-396
Efficient Instance Retrieval with Standard and Relational Path Indexing
Alexandre Riazanov and Andrei Voronkov
397-411
Monodic Temporal Resolution
Anatoly Degtyarev, Michael Fisher and Boris Konev
412-426
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
Renate A. Schmidt and Ullrich Hustadt
427-441
Schematic Saturation for Decision and Unification Problems
Christopher Lynch
442-457
Unification Modulo ACUI Plus Homomorphisms/Distributivity
Siva Anantharaman, Paliath Narendran and Michael Rusinowitch
458-472
Source-Tracking Unification
Venkatesh Choppella and Christopher T. Haynes
473-487
Optimizing Higher-Order Pattern Unification
Brigitte Pientka and Frank Pfenning
488-502
Decidability of Arity-Bounded Higher-Order Matching
Manfred Schmidt-Schauß
Back matter