ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 40, June 1998

Table of Contents
Message from the AAR President
Call for Participation: CADE-15
Workshop on Mechanization of Partial Functions
Workshop on Using AI Methods in Deduction
Workshop on Integration of Deduction Systems
Preliminary Call for Papers: FTP'98
Can Model Builders Help Logicians in Building Infinite Models?
Book Announcements:
Automated Deduction - A Basis for Applications
Term Rewriting and All That
Ethics, Computing, and Medicine

From the AAR President, Larry Wos...

Our summer issue of the AAR Newsletter features one of my favorite topics: using an automated reasoning program to assist the mathematician in solving difficult problems. My thanks to N. Peltier for this interesting article.

I hope AAR newsletter readers will also try the finite model generation exercise that Jian Zhang has provided.

Much of the rest of the newsletter is an invitation: you are invited--indeed, encouraged--to participate in CADE-15's lectures, workshops, and tutorials. As an added incentive, I note that Germany should be lovely at this time of year.

Call for Participation

CADE-15

The 15th International Conference on Automated Deduction will be held on July 5-10, 1998, in Lindau, Germany.

CADE is the major forum for the presentation of new research in all aspects of automated deduction. Logics of interest include propositional, first-order, higher-order, equational, classical, modal, temporal, dynamic, intuitionistic, constructive, linear, type theory, and meta-logics. Methods encompass resolution, tableaux, connection, unification, paramodulation, term constraints, decision procedures, induction, and model checking. Applications cover hardware and software development, systems verification, deductive databases, logic and functional programming, computer mathematics including algebra and geometry, deductive aspects in artificial intelligence. Special topics of interest involve logical frameworks, proof translation, human-computer interfaces, distributed deduction, and search heuristics.

CADE-15 features six full-day workshops (July 5) and three half-day workshops (July 6), four half-day tutorials (July 6), 24 research papers (July 6-9), 10 system descriptions (July 6-9), six invited lectures (July 6-10), and a one-day special symposium (July 10).

You are invited to attend CADE-15, to participate in the high-quality technical program, and to enjoy some great social events.

Full details about CADE-15, and an electronic registration form, are available on the Web at www.tu-darmstadt.de/cade-15 or via e-mail (cade-15@informatik.tu-darmstadt.de) or FAX (+49 6151 165326). Note: No hardcopy information or registration forms will be distributed unless explicitly requested.

CADE-15 Workshop on Mechanization of Partial Functions

In conjunction with CADE-15 (see above), a two-day workshop will be held on July 5-6 on the mechanization of partial functions.

Many practical applications of deduction systems in mathematics, computer science, and artificial intelligence rely on the correct and efficient treatment of partial functions. For this purpose different approaches--from workarounds for concrete situations to proper general treatments--have been developed.

There are essentially three approaches to treating partiality, which further subdivide into a multitude of specialized logical systems. In the first category, undefined expressions are syntactically excluded. In the second, they are disregarded or bypassed. In the third, partiality is taken serious, and this is reflected in the semantics and the calculus.

In order to make the distinction clear, let us look at the treatment of division by zero. In the first approach, terms like 1/0 are treated as syntactically ill-formed, for instance, by using a sorted logic. In the second approach, a value is assigned to 1/0, either a fixed value (e.g., 0) or an undetermined one. In both cases it is necessary to tolerate undesired theorems. In the third approach, terms like 1/0 are not defined and semantically either uninterpreted or interpreted by some error element. In the same manner, atomic formulae, containing such an undefined term, like 1/0=0 are not interpreted by a truth value (true or false) at all or are interpreted by a third truth value (undefined). In a two-valued variant atomic formulae containing an undefined term are evaluated to false. The workshop will discuss the advantages and disadvantages of each approach.

Those invited to attend the workshop must register for the workshop in conjunction with the CADE main conference. For further information, please contact Manfred Kerber, The University of Birmingham, UK (M.Kerber@cs.bham.ac.uk) or see the Web www.cs.bham.ac.uk/ mmk/cade98-partiality/.

CADE-15 Workshop on Using AI Methods in Deduction

Standard automated theorem proving techniques often fail, when applied to difficult problems. To achieve success, researchers have found it necessary to use specific knowledge from different sources: knowledge about the problem to solve and the domain it stems from, knowledge about the calculus and its weak spots, and knowledge about the behaviour of the particular prover used and its problems. In the past, many approaches have been developed to put this knowledge into provers. Naturally, concepts from other areas of artificial intelligence that deal with acquiring, handling and using of knowledge influenced the proposed approaches. Examples of such concepts that are currently under investigation are generation and use of knowledge bases supporting deduction systems and data mining techniques for analyzing prover behavior.

This workshop, to be held at CADE-15 (see above), is intended for researchers and developers of deduction systems, both fully automated and interactive, that are interested in the use of AI methods in their systems.

All participants of the workshop have to register for the main conference. For up-to-date information, see the Web www.uni-kl.de/AG-AvenhausMadlener/cade-ws.html.

CADE-15 Workshop on Integration of Deduction Systems

In contemporary design of deduction systems there is a clearly observable trend away from monolithic systems towards building integrated tools. Thus, the vast combinatorial power of fully automatic theorem provers might be opened for nonexpert users through the interface of interactive specification and verification tools. Also, real-world deduction problems tend to be so complex that no single methodology is likely to be successful. Though some high degree of maturity has been reaches by various subfields of automated deduction, the obstacles to integration are still nontrivial and diverse. The aim of this workshop is to describe the current state achieved in integration of deductive systems.

Topics will cover ongoing or completed research in the integration of deductive systems, investigations into theoretic concepts and calculi, and systems and experimental results.

Participants to the workshop should register using the electronic form on the CADE home page. Up-to-date information is available at i12www.ira.uka.de/Workshop/cfp.html.

FTP'98 - Preliminary Call for Papers

FTP'98, an international workshop on First-order Theorem Proving, will be held at Schloss Wilheminenberg, Vienna, Austria, on November 23-25, 1998.

FTP'98 is the second in a series of workshops intended to focus effort on first-order theorem proving as a core theme of automated deduction, and to provide a forum for presentation of very recent work and discussion of research in progress.

The workshop welcomes original contributions on theorem proving in classical, many-valued, and modal first-order logics, including resolution and tableau methods; equational reasoning and term-rewriting systems; constraint-based reasoning; unification algorithms for first-order theories; specialized decision procedures; propositional logic; abstraction; first-order constraints; complexity of theorem proving procedures; and applications of first-order theorem provers to problems in artificial intelligence, verification, mathematics, as well as other areas.

The technical program will include presentations of the accepted papers and invited talks. There will be ample time for questions and discussions in an informal atmosphere to foster the exchange of new ideas.

Authors are invited to submit an extended abstract of 5-8 pages. (See the FTP'98 home page www.logic.at/ftp98 for detailed instructions.) The submission deadline is August 31, 1998.

The extended abstracts that are accepted will be collected in a volume that will be distributed at the workshop. Additionally, the abstracts will be made available on the Web after the workshop. Authors of accepted abstracts will be invited to submit a full version, which will again be refereed. The selected papers will be published in the workshop proceedings; more details will become available soon.



Can Model Builders Help Logicians in Building Infinite Models?

Nicolas Peltier
Laboratory LEIBNIZ-IMAG
46, Avenue Félix Viallet 38031 Grenoble Cedex FRANCE
Nicolas.Peltier@imag.fr



Download Postscript file

Summary: Since automated theorem provers are becoming increasingly more powerful and easy to use, more and more difficult problems---which are interesting for mathematicians, logicians, or computer scientists---can be solved by using theorem provers, often with some help of the user (for choosing the inference rules, the strategy, etc.), This is also true for model building: already fifteen years ago, striking results were obtained with the help of theorem provers. Most of these results concern finite mathematics, where finite model builders were used to show the existence or nonexistence of {\em finite} structures satisfying some properties. In this work, we show how model-building methods can also be useful for showing the existence of {\em infinite} structures. More precisely, we show how to use an infinite model builder developed in our inference laboratory to build a model for a satisfiable formula introduced by Goldfarb in his proof of the unsolvability of the G class with identity.

Showing the Independence of An Axiom for Temporal Intervals by Model Generation

Jian Zhang
Email: zj@ox.ios.ac.cn

Download Postscript file

Summary: In the mid-1980s, Allen and Hayes proposed axiomatizing temporal intervals by using five axioms. Galton later developed a three-element structure that satisfies the first three axioms but falsifies the fifth. This brief article shows how SEM was used to generate one three-element model.

Book Announcements

Automated Deduction - A Basis for Applications

The nationwide research project Deduktion, funded by the Deutsche Forschungsgemeinschaft (DFG) for six years, brought together almost all research groups within Germany engaged in the field of automated reasoning. Intensive cooperation and exchange of ideas led to considerable progress both in the theoretical foundations and in the application of deductive knowledge. A three-volume book, edited by Wolfgang Bibel and Peter H. Schmitt, has now been published that covers the original contributions of the project.

Automated Deduction - A Basis for Applications
Volume I: Foundations - Calculi and Methods
(basic research in deduction and on the knowledge on which modern deductive systems are based
Volume II: Systems and Implementation Techniques
(techniques of implementation and details about system building)
Volume III: Applications
(applications of deductive techniques mainly, but not exclusively,
to mathematics and the verification of software)

The three volumes, published by Kluwer as part of the Applied Logic Series (Vols. 8-10), are intended to document and advance a development in the field of automated deduction that can now be observed all over the world. Rather than restricting the interest to purely academic research, the focus now is on the investigation of problems derived from realistic applications. In fact industrial applications are already pursued on a trial basis. In consequence the emphasis of the volumes is not on the presentation of the theoretical foundations of logical deduction as such, as in a handbook; rather, the books present the concepts and methods now available in automated deduction in a form that can be easily accessed by scientists working in applications outside of the field of deduction.

For more information, see the Web site: www.wkap.nl. The cost of the three-volume hardbound set (ISBN 0-7923-5132-0) until December 1, 1998, is NLG 895.00 / USD 480.00 / GBP 299.00.

Term Rewriting and All That

Franz Baader and Tobias Nipkow have published a new book Term Rewriting and All That (Cambridge University Press, 1998; ISBN 0-521-45520-0). As the back cover states, this is the first English language textbook offering an unified and self-contained introduction to the field of term rewriting.

The book discusses all the basic material (abstract reduction systems, termination, confluence, completion, and combination problems), but also some important and closely connected subjects: universal algebra, unification theory, and Gröbner bases. Most of the material is presented in the functional language Standard ML (an appendix contains a quick and easy introduction to ML).

Intended as a textbook, Term Rewriting and All That contains many examples and over 180 exercises.

The text is also an ideal reference book for professional researchers. It collects results reported in various conferences and journal articles in a unified notation, and gives detailed proofs of almost all the theorems. Each chapter also closes with a ``gentle guide'' to the literature.

Ethics, Computing, and Medicine

Those interested in new technology and controversy may wish to read the book Ethics, Computing, and Medicine, edited by K. W. Goodman (Cambridge University Press, 1998; ISBN 0-521-46905-8). This book addresses the full ranges of ethical issues that arise when intelligent machines are used in medicine, nursing, psychology, and allied health professions.

Included are chapters on bioethics and health informatics; medical informatics and human values; responsibility for computer-based decisions in health care; evaluating medical information systems; health care information; ethical challenges in the use of decision-support software in clinical practice; outcomes, futility, and health policy research; and meta-analysis.

Throughout, the contributors suggest practical approaches to difficult problems, including the appropriate use of decision-support systems.