CADE Workshops
Tuesday, 30 July 1996

The Workshop Program consists of six workshops and one tutorial. These workshops are open to everyone. If you wish to attend a workshop you must first contact the Workshop Organizing Committee.

The registration fee for a workshop is $50.00 for registration by 21 June, 1996. The registration fee for registration after this date is $80.00.

Workshops will only be held if there are a minimum of 10 registrants by 21 June, 1996.

____________

Workshop WP-1: 9:00-17:00
Term Schematizations and Their Applications

A common phenomenon throughout all areas dealing with first order terms (particularly in automated deduction) are infinite sequences of structurally similar terms. One characteristic of computer science is its emphasis on finite structures. Consequently, various formalisms and methods have been proposed to capture these sequences by finite means, among them schematizations of terms.

A schematization is a finite expression together with a mechanism for effectively generating the elements of the set. In addition, it should be possible to compute the unifying intersection of infinite term sets by manipulating their finite schematizations.

The aim of the workshop is to bring together researchers working on schematizations and to discuss the different approaches as well as their applications in clausal theorem proving, term rewriting, unification theory, finite model building, and other areas.

Program Committee: Miki Hermann (CRIN-CNRS Nancy & INRIA Lorraine, France); Gernot Salzer (Technische Universität Wien, Austria) schema@logic.tuwien.ac.at.

For further information and program click here.

____________

Workshop WP-2: 9:00-17:00
Visual Reasoning

The idea behind the workshop is to help make automated reasoning more widely accepted and applicable. Visualization can help achieve this. To obtain the best results researchers in the field of automated reasoning should actively participate in the development of the required tools and techniques. The workshop will be a forum to bring together the scattered attempts that have been pursued along these lines in a number of locations. The application of visualization in the context of formal reasoning certainly covers a broader audience, so we encourage participants to also enroll in other parts of the Federated Logic Conference.

The workshop addresses all issues involved with applying visiualization in the context of formal reasoning, specification, or verification. Such topics include, but are not limited to:

Program Committee: Gerard Allwein (Indiana University, USA) gtall@phil.indiana.edu; Joachim Posegga (Deutsche Telekom Research, Germany) Posegga@FZ.Telekom.DE; Peter H. Schmitt (University of Karlsruhe, Germany) PSchmitt@ira.uka.de.

For further information click here.

____________

Workshop WP-3: 9:00-17:00
Automation of Proofs by Mathematical Induction

The workshop will cover research on mathematical induction and its applications within formal methods. It will consist of debates on several `hot topics'. Speakers will be chosen who represent different viewpoints on these topics. After they have introduced the arguments, the debate will be thrown open for general discussion. The exact list of topics is still to be determined, but might include:

Program Committee: Dieter Hutter (DFKI, Germany) hutter@dfki.uni-sb.de; David McAllester (AT&T Laboratories, USA) dmac@research.att.com; Christoph Walther (Technische Hochschule Darmstadt, Germany) walther@inferenzsysteme.informatik.th-darmstadt.de.

For further information click here.

____________

Workshop WP-4: 9:00-17:00
Empirical Studies in Logic Algorithms

This workshop has been cancelled.

Implementation and experimentation are vital tasks in automated theorem proving research. Heuristics, strategies, and even proof procedures have to show their advantages in implementations and, if appropriate, in comparison to other systems. On the other hand experimental results have influence on theoretical studies, e.g. heuristics for Davis-Putnam algorithms, resolution strategies, or indexing techniques.

This workshop should give helpful hints and tips to such major tasks as:

Program Committee: Ulf Dunker (University of Paderborn, Germany) dunker@uni-paderborn.de; Hans Kleine Büning (University of Paderborn, Germany) kbcsl@uni-paderborn.de; Theo Lettman (University of Paderborn, Germany) lettmann@uni.paderborn.de.

For further information click here.

____________

Workshop WP-5: 9:00-17:00
Mechanization of Partial Functions

Many practical applications of deduction systems in mathematics and computer science rely on the correct and efficient treatment of partial functions. There is a rich variety of approaches for dealing with partial functions and the undefined expressions that often result from their application. Ranging from workarounds for concrete situations to proper general treatments, these approaches have their own advantages and disadvantages. For example, some can be used in standard logical formalisms, while others require new formalisms. The purpose of the workshop is to discuss the different approaches and to compare their advantages and disadvantages.

Program Committee: William Farmer (MITRE Corporation, USA) farmer@mitre.org; Manfred Kerber (University of Birmingham, UK) M.Kerber@cs.bham.ac.uk; Michael Kohlhase (University of the Saarlandes, Germany) kohlhase@cs.uni-sb.de.

For further information and program click here.

____________

Workshop WP-6: 9:00-17:00
Proof Search in Type-Theoretic Languages

Much recent work has been devoted to type theory and its applications to proof and program development in various logical frameworks. This workshop focuses on proof search in type-theoretic languages. Such languages are logical frameworks, issued from classical, intuitionistic or linear logics, for representing proofs and in some cases formalizing connections between proofs and programs.

The purpose of this workshop is to discuss recent results in the area and to bring together researchers interested in all aspects of proof search in type-theoretic languages and their underlying logics, including, but not limited to, the following topics: foundations of proof search, techniques and concepts related to proof construction, logic programming, proof synthesis vs program synthesis, applications, equational theories and rewriting, decision procedures, environments for formal proof development.

Program Committee: D. Galmiche (CRIN-CNRS Nancy, France) Didier.Galmiche@loria.fr; F. Pfenning (Carnegie Mellon University, USA); N. Shankar (SRI, USA); J. Smith (Chalmers Univ Göteborg, Sweden); L. Wallen (Oxford University, UK).

For further information and program click here.

____________

Tutorial WP-7: 9:00-12:00
Equality Reasoning in Semantic Tableaux and
Other Sequent-Based Calculi

by
Anatoli Degtyarev (Uppsala University, Sweden)
Andrei Voronkov (Uppsala University, Sweden)
email: voronkov@csd.uu.se

The treatment of equality in sequent-based machine-oriented calculi has a long history started by Kanger in 1957. The theoretical basis for handling equality in sequent-based calculi has been developed by Swedish logicians in the 1950s (Kanger and Prawitz) and by Soviet logicians in the 1960s (Orevkov, Maslov et.al.).

The next generation of work in this area is based on rigid unification (Gallier et.al.) formulated in 1987. Recently, this area witnessed rapid development of new results and techniques (Degtyarev and Voronkov, Matiyasevich, Voda and Komara, Plaisted), including new results on rigid unification, the equality elimination method, rigid superposition and rigid paramodulation.

The techniques of equality reasoning presented in the tutorial are applicable to all known sequent-based methods of automated deduction, including the tableau method, the connection method, model elimination and the inverse method. We shall illustrate main results and ideas on the tableau method and on the inverse method (as a typical non-local top-down and a typical local bottom-up search method in sequent calculi).

For further information click here.

____________

[Next] [Prev] [Contents] FLoC homepage