The 1996 International Conference on Automated Deduction (CADE-13) is the 13th conference in this series. CADE is the major forum for the presentation of new research results in all aspects of automated deduction and includes descriptions of working reasoning systems and problem sets that provide innovative, challenging tests for automated reasoning systems. The contributed presentations at CADE-13 include 46 refereed papers and 15 refereed systems abstracts to be given in two parallel sessions. Demonstrations of these systems will be held during CADE as is now traditional. CADE-13 will also feature two plenary addresses from Dana Scott and Harald Ganzinger, a plenary address with CAV from John Rushby and a panel on the future of automated deduction being organised by Don Loveland and Deepak Kapur. One highlight of the conference is likely to be the Theorem Proving Competition being organised by Geoff Sutcliffe and Christian Suttner. The proceedings of CADE will be published by Springer-Verlag.

Program Chairs: Michael McRobbie, John Slaney (Australian National University)

Local Arrangements Chair: Amy Felty (Bell Labs)

Program Committee: O. Astrachan (Duke), J. Avenhaus (Kaiserslautern), L. Bachmair (Stony Brook), D. Basin (Max-Planck), W. Bibel (Darmstadt), B. Buchberger (Linz), F. Bry (Munich), R. Caferra (Grenoble), K. S. Choi (KAIST), A. Cohn (Leeds), L. Farinas del Cerro (Toulouse), W. Farmer (MITRE), A. Felty (Bell Labs), M. Fitting (CUNY), M. Fujita (MRI), S. Garland (MIT), F. Giunchiglia (IRST), E. Gunter (Bell Labs), R. Hasegawa (Kyushu), L. Henschen (North Western), L. Hines (Texas), S. Hölldobler (Dresden), M. Kaufmann (Motorola), A. Leitsch (Vienna), E. Lusk (Argonne), U. Martin (St. Andrews), D. McAllester (AT&T Laboratories), W. McCune (Argonne), H.-J. Ohlbach (Max-Planck), J. Posegga (Karlsruhe), W. Pase (ORA Canada), F. Pfenning (Carnegie Mellon), F. Pirri (Rome), D. Plaisted (North Carolina), U. Reddy (Illinois), M. Rusinowitch (INRIA), K. Satoh (Hokkaido), J. Schumann (Munich), C. Schwind (Marseille), N. Shankar (SRI), J. Siekmann (Saarbrücken), A. Smaill (Edinburgh), G. Smolka (Saarbrücken), M. Stickel (SRI), G. Sutcliffe (James Cook), E. Tiden (Siemens), A. Voronkov (Uppsala), L. Wallen (Oxford), D. Wang (Grenoble), H. Zhang (Iowa).

Email: cade13@cisr.anu.edu.au (general), cade13-la@cisr.anu.edu.au (local arrangements)

FLoC Plenary Session: 20:00-21:30. Chair: M.Y. Vardi.

Calculi for Interactions
R. Milner (Cambridge University, United Kingdom)

Saturation-based Theorem Proving: Past Successes and Future Potential
Harald Ganzinger (MPI Saarbrücken, Germany)

Abstract: Saturation means to compute the closure of a given set of formulas under a given set of inference rules. Resolution, Knuth/Bendix completion, and Superposition are major examples of saturation-based, automated theorem proving methods. More recently, considerable progress has made in this area. New theoretical insight has been gained. In particular the nature of redundancy and of mechanisms for avoiding redundancy is now better understood. This has many applications, both in theory and in practice. New provers based on these ideas are emerging and seem to perform well, outperforming existing automated provers in many respects. The talk surveys some of the theoretical results, describes experience gained from experimentation, and outlines problems and potential for future research.

Coffee Break: 10:15-10:45.

Parallel Session 1A: 10:45-12:15. Chair: J. Avenhaus.

A resolution theorem prover for intuitionistic logic
T. Tammet (University of Goteborg, Sweden)

Proof-terms for classical and intuitionistic resolution
D. Pym (University of London, UK), E. Ritter (Oxford University, UK) & L. Wallen (Oxford University, UK)

On the proof-search in intuitionistic logic with equality, or back to simultaneous Rigid E-Unification
A. Voronkov (Uppsala University, Sweden)

Parallel Session 1B: 10:45-12:15. Chair: D. Basin.

Extensions to a generalization critic for inductive proof
A. Ireland (Heriot-Watt University, Scotland) & A. Bundy (University of Edinburgh, Scotland)

Learning domain knowledge to improve theorem proving
J. Denzinger (University of Kaiserslautern, Germany) & S. Schulz (TU München, Germany)

Patching faulty conjectures
M. Protzen (Technische Hochschule Darmstadt, Germany)

Lunch Break: 12:15-14:00.

Parallel Session 2A: 14:00-15:30. Chair: D. McAllester.

Internal analogy in theorem proving
Erica Melis (University of the Saarlandes, Germany) & Jon Whittle (University of Edinburgh, UK)

Termination of theorem proving by reuse
T. Kolbe (Technische Hochschule Darmstadt, Germany) & C. Walther (Technische Hochschule Darmstadt, Germany)

Termination of algorithms over non-freely generated data types
C. Sengler (DFKI, Germany)

Parallel Session 2B: 14:00-15:30. Chair: W. Farmer.

ABSFOL: A proof checker by abstraction
F. Giunchiglia (IRST, Italy) & A. Villafiorita (Stanford University, USA)

SPASS & FLOTTER
C. Weidenbach (MPI Saarbrücken, Germany), B. Gaede (MPI Saarbrücken, Germany) & G. Rock (MPI Saarbrücken, Germany)

The design of the CADE-13 ATP system competition
C. Suttner (TU München, Germany) & G. Sutcliffe (James Cook University, Australia)

SCAN - Elimination of predicate quantifiers system description
H.J. Ohlbach (MPI Saarbrücken, Germany)

GEOTHER: A geometry theorem prover
Dongming Wang (LIFIA Institut Imag, France)

Coffee Break: 15:30-16:00.

Parallel Session 3A: 16:00-17:30. Chair: U. Martin.

Structuring metatheory on inductive definitions
D. Basin (MPI Saarbrücken, Germany) & S. Matthews (MPI Saarbrücken, Germany)

An embedding of Ruby in Isabelle
O. Rasmussen (Technical University of Denmark, Denmark)

Mechanical verification of mutually recursive procedures
P. Homeier (UCLA, USA) & D. Martin (UCLA, USA)

Parallel Session 3B: 16:00-17:30. Chair: G. Sutcliffe.

FasTraC - A decentralized traffic control system based on logic programming
G. Felici (University of Texas, USA), G. Rinaldi (CNR-IASI, Italy) & K. Truemper (University of Texas, USA)

Presenting machine-found proofs
X. Huang (University of the Saarlandes, Germany) & A. Fiedler (University of the Saarlandes, Germany)

MUltlog 1.0: Towards an expert system for many-valued logics
G. Salzer (TU Wien, Austria)

CtCoq: a system presentation
J. Bertot (INRIA Sophia-Antipolis, France) & Y. Bertot (INRIA Sophia-Antipolis, France)

An introduction to geometry expert
Shang-Ching Chou (Wichita State University, USA), Xiao-Shan Gao (Wichita State University, USA) & Jing-Zhong Zhang (Wichita State University, USA)

SiCoTHEO: Simple Competitive Parallel Theorem Provers
J. Schumann (Techniche University of München, Germany)

Business Meeting: 17:30-20:00.

What Can We Hope to Achieve From Automated Deduction?
Dana S. Scott (Carnegie Mellon University, USA)

Abstract: We have been fortunate that the capacity and speed of computers has increased so quickly over the last decade. Many research groups around the world have been able to make new, stronger implementations and to solve new problems. Many limitations still exist, however, and as a field we must decide on the designs and objectives for the next period of work. Should we give more attention to user interfaces? Should we make better connections to computer algebra? Should we make strong efforts to construct large-scale knowledge bases? Should we investigate non-standard or non-classical logics? Should we be concerned with pedagogical applications? Where should we look for other applications? All of these questions - and others - need to be answered, and a survey of possibilities will be presented.

Coffee Break: 10:15-10:45.

Parallel Session 4A: 10:45-12:15. Chair: M. Rusinowitch.

Unification algorithms cannot be combined in polynomial time
M. Hermann (CRIN (CNRS), France) & P.G. Kolaitis (UC Santa Cruz, USA)

Unification and matching modulo nilpotence
Q. Guo (SUNY Albany, USA), P. Narendran (SUNY Albany, USA) & D. Wolfram (ANU, Australia)

An improved lower bound for the elementary theories of trees
S. Vorobyov (MPI Saarbrücken, Germany)

Parallel Session 4B: 10:45-12:15. Chair: F. Giunchiglia.

INKA: The next generation
D. Hutter (DFKI, Germany) & C. Sengler (DFKI, Germany)

XRay: A prolog technology default theorem prover
T. Schaub (Université d'Angers, France), S. Bruning (ZB Informationssysteme, Germany), T. Linke (University of Bremen, Germany) & P. Nicolas (Université d'Angers, France)

IMPS: An Updated System Description
W. Farmer (The Mitre Corporation, USA), J. Guttman (The Mitre Corporation, USA) & J. Thayer (The Mitre Corporation, USA)

The tableau-based theorem prover 3 TAP, version 4.0
B. Beckert (University of Karlsruhe, Germany), R. Hahnle (University of Karlsruhe, Germany), P. Oel (University of Karlsruhe, Germany) & M. Sulzmann (University of Karlsruhe, Germany)

Generating models by SEM
J. Zhang (University of Iowa, USA) & H. Zhang (University of Iowa, USA)

Lunch Break: 12:15-14:00.

Parallel Session 5A: 14:00-15:30. Chair: A. Felty.

Optimizing proof search in model elimination
J. Harrison (Åbo Akademi University, Finland)

An abstract machine for fixed-order dynamically stratified programs
K. Sagonas (SUNY Stony Brook, USA), T. Swift (SUNY Stony Brook, USA) & D. Warren (SUNY Stony Brook, USA)

Unification in pseudo-linear sort theories is decidable
C. Weidenbach (MPI Saarbrücken, Germany)

Parallel Session 5B: 14:00-15:30. Chair: S. Garland.

Theorem proving with group presentations: Examples and questions
U. Martin (University of St. Andrews, Scotland)

Transforming termination by self-labelling
A. Middledorp (University of Tsukuba, Japan), H. Ohsaki (University of Tsukuba, Japan) & H. Zantema (Utrecht University, Netherlands)

Theorem proving in cancellative abelian monoids (extended abstract)
H. Ganzinger (MPI Saarbrücken, Germany) & U. Waldmann (MPI Saarbrücken, Germany)

Coffee Break: 15:30-16:00.

Parallel Session 6A: 16:00-17:30. Chair: J. Schumann.

On the practical value of different definitional translations to normal form
U. Egly (TU Wien, Austria) & T. Rath (Technische Hochschule Darmstadt, Germany)

On converting non-classical matrix proofs into sequent-style systems
C. Kreitz (Technische Hochschule Darmstadt, Germany) & S. Schmitt (Technische Hochschule Darmstadt, Germany)

Efficient model generation through compilation
H. Schuetz (Ludwig-Maximilians University of München, Germany) & T. Geisler (Ludwig-Maximilians University of München, Germany)

Parallel Session 6B: 16:00-17:30. Chair: D. Wang.

Algebra and automated deduction
S. Linton (University of St. Andrews, Scotland), U. Martin (University of St. Andrews, Scotland), P. Prohle (University of St. Andrews, Scotland) & D. Shand (University of St. Andrews, Scotland)

On Shostak's decision procedure for combinations of theories
N. Shankar (SRI International, USA), D. Cyrluk (SRI International, USA) & P. Lincoln (SRI International, USA)

Ground resolution with group computations on semantic symmetries
T. Boy de la Tour (LIFIA-IMAG, France)

Joint Banquet with CAV: 18:30-23:00. Dinner speech by Amir Pnueli (Weizmann Institute, Israel), ``The Potential and Sensible Scopes of Formal Methods.''

Automated Deduction and Formal Methods
J. Rushby (SRI International, USA)

Coffee Break: 10:15-10:45.

Parallel Session 7A: 10:45-12:15. Chair: D. Plaisted.

A new method for logical compilation: the achievement by cycle search
Olivier Roussel (LIFL CNRS, France) & Philippe Mathieu (LIFL CNRS, France)

Rewrite semantics for production rule systems: theory and applications
W. Snyder (Boston University, USA) & J.G. Schomolze (Tufts University, USA)

Experiments in the heuristic use of past proof experience
Matthias Fuchs (University of Kaiserslautern, Germany)

Parallel Session 7B: 10:45-12:15. Chair: U. Reddy.

Lemma Discovery in automating induction
D. Kapur (SUNY Albany, USA) & M. Subramaniam (SUNY Albany, USA)

Advanced indexing operations on substitution trees
P. Graf (MPI Saarbrücken, Germany) & C. Meyer (MPI Saarbrücken, Germany)

Semantic trees revisted - some new completeness results
C.G. Fermuller (Stanford University, USA)

Lunch Break: 12:15-13:30.

Excursion: 13:30.

Does Automated Deduction have a Future?

Abstract: Does the field of automated deduction have to sharply shift its research focus to keep its credibility (and its funding)? A panel will explore the nature and goals of automated deduction, its present and future applications, and linkages with other fields. It will attempt to identify areas where automated deduction can be expected to make significant contributions and problems that must be surmounted in order to do so. It will kick-off with a summary of the discussion of an NSF-sponsored workshop on the future directions of automated deduction held in April in Chicago. Panelists would include members of the workshop steering committee as well as other researchers. The panel presentation will be short enough to leave most of the time for discussion with audience participation.

Coffee Break: 10:15-10:45.

Parallel Session 8A: 10:45-12:15. Chair: L. Farinas del Cerro.

Building decision procedures for modal logics from propositional decision procedures - the case study of modal K*
F. Giunchiglia (IRST, Italy) & R. Sebastiani (University of Genoa, Italy)

Resolution-based calculi for modal and temporal logics
A. Nonnengart (MPI Saarbrücken, Germany)

Tableaux and algorithms for propositional dynamic logic with converse
G. De Giacomo (Universtà di Roma, Italy) & F. Massacci (Universtà di Roma, Italy)

Parallel Session 8B: 10:45-12:15. Chair: L. Wallen.

Reflection of formal tactics in a deductive reflection framework
H. Ruess (University of Ulm, Germany)

Walther Recursion
D. McAllester (AT&T Laboratories, USA) & K. Arkoudas (MIT, USA)

Proof search with set variable instantiation in the calculus of constructions
A. Felty (Bell Labs, USA)

Lunch Break: 12:15-14:00.

Parallel Session 9A: 14:00-15:30. Chair: A. Voronkov.

Search strategies for resolution in temporal logic
C. Dixon (Manchester Metropolitan University, UK)

Optimal axiomatizations for multiple-valued operations and quantifiers based on semi-lattices
G. Salzer (TU Wien, Austria)

Grammar Specification in Categorical Logics and Theorem Proving
S. Luz-Filho (Edinburgh University, Scotland)

Parallel Session 9B: 14:00-15:30. Chair: E. Gunter.

Path Indexing for AC-Theories
P. Graf (MPI Saarbrücken, Germany)

More Church-Rosser Proofs (in Isabelle/HOL)
T. Nipkow (TU München, Germany)

Partitioning methods for satisfiability testing on large formulas
Tai Joon Park (UC Santa Cruz, USA) & A. van Gelder (UC Santa Cruz, USA)

Coffee Break: 15:30-16:00.

Business Meeting: moved to Wednesday evening, 31 July.