19. CADE 2003: Miami Beach, Florida, USA

Invited Talk

• Edmund M. Clarke:
  SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. 1
  

Session 2

• José Meseguer, Miguel Palomino, Narciso Martí-Oliet:
  Equational Abstractions. 2-16
  
• Jürgen Giesl, Deepak Kapur:
  Deciding Inductive Validity of Equations. 17-31
  
• Nao Hirokawa, Aart Middeldorp:
  Automating the Dependency Pair Method. 32-46
  
• Konstantin Korovin, Andrei Voronkov:
  An AC-Compatible Knuth-Bendix Order. 47-59
  

Session 3

• Carsten Lutz, Ulrike Sattler, Lidia Tendera:
  The Complexity of Finite Model Reasoning in Description Logics. 60-74
  
• Guoqiang Pan, Moshe Y. Vardi:
  Optimizing a BDD-Based Modal Solver. 75-89
  
• Jan Hladik, Ulrike Sattler:
  A Translation of Looping Alternating Automata into Description Logics. 90-105
  

Session 4

• Karl Crary, Susmit Sarkar:
  Foundational Certified Code in a Metalogical Framework. 106-120
  
• Farhad Mehta, Tobias Nipkow:
  Proving Pointer Programs in Higher-Order Logic. 121-135
  
• Dimitri Hendriks, Vincent van Oostrom:
  adbmal. 136-150
  
• Aaron Stump:
  Subset Types and Partial Functions. 151-165
  

Session 5

• Greg Nelson:
  Reasoning about Quantifiers by Matching in the E-graph. 166
  

Session 6

• Sumit Gulwani, George C. Necula:
  A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. 167-181
  
• Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann:
  Superposition Modulo a Shostak Theory. 182-196
  
• Sava Krstic, Sylvain Conchon:
  Canonization for Disjoint Unions of Theories. 197-211
  
• Christophe Ringeissen:
  Matching in a Class of Combined Non-disjoint Theories. 212-227
  

Session 7

• Johan G. F. Belinfante:
  Reasoning about Iteration in Gödel's Class Theory. 228-242
  
• Panagiotis Manolios, Daron Vroon:
  Algorithms for Ordinal Arithmetic. 243-257
  
• Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge:
  Certifying Solutions to Permutation Group Problems. 258-273
  

System Descriptions

• Ullrich Hustadt, Boris Konev:
  TRP++2.0: A Temporal Resolution Prover. 274-278
  
• Lucas Dixon, Jacques D. Fleuriot:
  IsaPlanner: A Prototype Proof Planner in Isabelle. 279-283
  
• Peter Baumgartner, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner:
  'Living Book': -'Deduction', 'Slicing', 'Interaction'. 284-288
  
• Simon Colton, Sophie Huczynska:
  The Homer System. 289-294
  

CASC-19 Results

• Geoff Sutcliffe, Christian B. Suttner:
  The CADE-19 ATP System Competition. 295-296
  

Invited Talk

• Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen:
  Proof Search and Proof Check for Equational and Inductive Theorems. 297-316
  

System Descriptions

• Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies:
  The New WALDMEISTER Loop at Work. 317-321
  
• Christoph Walther, Stephan Schweitzer:
  About VeriFun. 322-327
  
• Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth:
  How to Prove Inductive Theorems? QUODLIBET! 328-333
  

Invited Talk

• Anthony G. Cohn:
  Reasoning about Qualitative Representations of Space and Time. 334
  

Session 13

• Harald Ganzinger, Jürgen Stuber:
  Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. 335-349
  
• Peter Baumgartner, Cesare Tinelli:
  The Model Evolution Calculus. 350-364
  
• Hans de Nivelle:
  Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. 365-379
  
• Alexandre Riazanov, Andrei Voronkov:
  Efficient Instance Retrieval with Standard and Relational Path Indexing. 380-396
  

Session 14

• Anatoli Degtyarev, Michael Fisher, Boris Konev:
  Monodic Temporal Resolution. 397-411
  
• Renate A. Schmidt, Ullrich Hustadt:
  A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. 412-426
  
• Christopher Lynch:
  Schematic Saturation for Decision and Unification Problems. 427-441
  

Session 15

• Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch:
  Unification Modulo ACU I Plus Homomorphisms/Distributivity. 442-457
  
• Venkatesh Choppella, Christopher T. Haynes:
  Source-Tracking Unification. 458-472
  
• Brigitte Pientka, Frank Pfenning:
  Optimizing Higher-Order Pattern Unification. 473-487
  
• Manfred Schmidt-Schauß:
  Decidability of Arity-Bounded Higher-Order Matching. 488-502