CADE-19 in Miami

28 July - 2 August 2003

In the sunshine ... On the beach

Paper Schedule

Session 1: Wednesday 30th, 09:00-10:00 - Chair: Harald Ganzinger
09:00-10:00 Invited Talk: SAT-based Counterexample Guided Abstraction Refinement in Model Checking
Edmund Clarke
Session 2: Wednesday 30th, 10:30-12:30 - Chair: Claude Kirchner
10:30-11:00 Equational Abstractions
Jose Meseguer, Miguel Palomino, Narciso Marti-Oliet
11:00-11:30 Deciding Inductive Validity of Equations
Jürgen Giesl, Deepak Kapur
11:30-12:00 Automating the Dependency Pair Method
Nao Hirokawa, Aart Middeldorp
12:00-12:30 AC-compatible Knuth-Bendix Orderings
Konstantin Korovin, Andrei Voronkov
Session 3: Wednesday 30th, 14:00-15:30 - Chair: Renate Schmidt
14:00-14:30 The Complexity of Finite Model Reasoning in Description Logics
Carsten Lutz, Ulrike Sattler, Lidia Tendera
14:30-15:00 Optimizing a BDD-based Modal Solver
Guoqiang Pan, Moshe Y. Vardi
15:00-15:30 A Translation of Looping Alternating Automata into Description Logics
Jan Hladik, Ulrike Sattler
Session 4: Wednesday 30th, 16:00-18:00 - Chair: Frank Pfenning
16:00-16:30 Foundational Cerfied Code in a Metalogical Framework
Karl Crary, Susmit Sarkar
16:30-17:00 Proving Pointer Programs in Higher-Order Logic
Farhad Mehta, Tobias Nipkow
17:00-17:30 Adbmal
Dimitri Hendriks, Vincent van Oostrom
17:30-18:00 Subset types and partial functions
Aaron Stump
Session 5: Thursday 31st, 09:00-10:00 - Chair: Chris Lynch
09:00-10:00 Invited Talk: Reasoning About Quantifiers by Matching in the E-graph
Greg Nelson
Session 6: Thursday 31st, 10:30-12:30 - Chair: Cesare Tinelli
10:30-11:00 A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols
Sumit Gulwani, George C. Necula
11:00-11:30 Superposition modulo a Shostak Theory
Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann
11:30-12:00 Canonization for Disjoint Unions of Theories
Sava Krstic, Sylvain Conchon
12:00-12:30 Matching in a Class of Combined Non-Disjoint Theories
Christophe Ringeissen
Session 7: Thursday 31st, 14:00-15:30 - Chair: Carsten Schürmann
14:00-14:30 Reasoning About Iteration in Goedel's Class Theory
Johan G. F. Belinfante
14:30-15:00 Algorithms for Ordinal Arithmetic
Panagiotis Manolios, Daron Vroon
15:00-15:30 Certifying Solutions to Permutation Group Problems
Arjeh Cohen, Scott Murray, Martin Pollet, Volker Sorge
Session 8: Thursday 31st, 16:00-17:00 - Chair: Tony Cohn
16:00-16:20 TRP 2.0: A Temporal Resolution Prover
Ullrich Hustadt, Boris Konev
16:20-16:40 IsaPlanner: A Prototype Proof Planner in Isabelle
Lucas Dixon, Jacques Fleuriot
16:40-17:00 `Living Book` :- `Deduction`, `Slicing`, `Interaction`.
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, Alex Sinner
17:00-17:20 The HOMER System
Simon Colton, Sophie Huczynska
Session 9: Thursday 31st, 17:30-18:30
17:30-18:00 Presentation of CASC Results
Geoff Sutcliffe, Christian Suttner
18:00-18:30 Presentations about the Winning Systems
Developers
Session 10: Friday 1st, 14:30-15:30 - Chair: Deepak Kapur
14:30-15:30 Invited Talk: Proof Search and Proof Check for Equational and Inductive Theorems
Hélène Kirchner
Session 11: Friday 1st, 16:00-17:00 - Chair: Reinhold Letz
16:00-16:20 The New Waldmeister Loop at Work
Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies
16:20-16:40 About VeriFun
Christoph Walther, Stephan Schweitzer
16:40-17:00 How to Prove Inductive Theorems? QuodLibet!
Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth
Herbrand award ceremony: Friday 1st, 17:00-18:00
17:00-17:15 Presentation of the Herbrand award to Peter Andrews
Frank Pfenning, Vice-president of CADE Inc.
17:15-18:00 Acceptance speech
Peter Andrews
Session 12: Saturday 2nd, 09:00-10:00 - Chair: Ilkka Niemela
09:00-10:00 Invited Talk: Reasoning about Qualitative Representations of Space and Time
Tony Cohn
Session 13: Saturday 2nd, 10:30-12:30 - Chair: Roberto Nieuwenhuis
10:30-11:00 Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
Harald Ganzinger, Jürgen Stuber
11:00-11:30 The Model Evolution Calculus
Peter Baumgartner, Cesare Tinelli
11:30-12:00 Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
Hans de Nivelle
12:00-12:30 Efficient Instance Retrieval with Standard and Relational Path Indexing
Alexandre Riazanov, Andrei Voronkov
Session 14: Saturday 2nd, 14:00-15:30 - Chair: Toby Walsh
14:00-14:30 Monodic Temporal Resolution
Anatoly Degtyarev, Michael Fisher, Boris Konev
14:30-15:00 A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
Renate A. Schmidt, Ullrich Hustadt
15:00-15:30 Schematic Saturation for Decision and Unification Problems
Christopher Lynch
Session 15: Saturday 2nd, 16:00-18:00 - Chair: Peter Baumgartner
16:00-16:30 Unification modulo ACUI plus Homomorphisms/Distributivity
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
16:30-17:00 Source-tracking Unification
Venkatesh Choppella, Christopher T. Haynes
17:00-17:30 Optimizing Higher-order Pattern Unification
Brigitte Pientka, Frank Pfenning
17:30-18:00 Decidability of Arity-Bounded Higher-Order Matching
Manfred Schmidt-Schauß