CADE-19 in Miami 28 July - 2 August 2003 In the sunshine ... On the beach

• Unification modulo ACUI plus Homomorphisms/Distributivity
  Siva Anantharaman, Paliath Narendran, Michael Rusinowitch

• Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
  Harald Ganzinger, Jürgen Stuber

• A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
  Renate A. Schmidt, Ullrich Hustadt

• Matching in a Class of Combined Non-Disjoint Theories
  Christophe Ringeissen

• Reasoning about iteration in Goedel's class theory
  Johan G. F. Belinfante

• Optimizing a BDD-based Modal Solver
  Guoqiang Pan, Moshe Y. Vardi

• Efficient instance retrieval with standard and relational path indexing
  Alexandre Riazanov, Andrei Voronkov

• AC-compatible Knuth-Bendix Orderings
  Konstantin Korovin, Andrei Voronkov

• Canonization for disjoint unions of theories
  Sava Krstic, Sylvain Conchon

• Optimizing higher-order pattern unification
  Brigitte Pientka, Frank Pfenning

• Automating the Dependency Pair Method
  Nao Hirokawa, Aart Middeldorp

• Proving Pointer Programs in Higher-Order Logic
  Farhad Mehta, Tobias Nipkow

• The Complexity of Finite Model Reasoning in Description Logics
  Carsten Lutz, Ulrike Sattler, Lidia Tendera

• Deciding Inductive Validity of Equations
  Jürgen Giesl, Deepak Kapur

• Extraction of Short Natural Deduction Proofs from Resolution without Using Choice Axioms
  Hans de Nivelle

• Certifying solutions to permutation group problems
  Arjeh Cohen, Scott Murray, Martin Pollet, Volker Sorge

• Monodic Temporal Resolution
  Anatoly Degtyarev, Michael Fisher, Boris Konev

• A Translation of Alternating Automata to Description Logics
  Jan Hladik, Ulrike Sattler

• Decidability of Arity-Bounded Higher-Order Matching
  Manfred Schmidt-Schauß

• A Metalogical Approach to Foundational Certified Code
  Karl Crary, Susmit Sarkar

• Equational Abstractions
  Jose Meseguer, Miguel Palomino, Narciso Marti-Oliet

• Adbmal
  Dimitri Hendriks, Vincent van Oostrom

• Algorithms for Ordinal Arithmetic
  Panagiotis Manolios, Daron Vroon

• The Model Evolution Calculus
  Peter Baumgartner, Cesare Tinelli

• Superposition modulo a Shostak Theory
  Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann

• Source-tracking Unification
  Venkatesh Choppella, Christopher T. Haynes

• A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols
  Sumit Gulwani, George C. Necula

• Subset types and partial functions
  Aaron Stump

• Schematic Saturation for Decision and Unification Problems
  Christopher Lynch

System Descriptions

• The HOMER System
  Simon Colton, Sophie Huczynska

• How to prove inductive theorems? Quodlibet!
  Jürgen Avenhaus, Ulrich Kuehler, Tobias Schmidt-Samoa, Claus-Peter Wirth

• 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

• About VeriFun
  Christoph Walther, Stephan Schweitzer

• The New Waldmeister Loop at Work
  Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies