NEWSLETTER
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.
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, 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.
Nicolas Peltier
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.
Jian Zhang
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.
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
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.
Call for Participation
FTP'98 - Preliminary Call for Papers
Can Model Builders Help Logicians in Building Infinite Models?
Laboratory LEIBNIZ-IMAG
46, Avenue Félix Viallet 38031
Grenoble Cedex FRANCE
Nicolas.Peltier@imag.fr
Showing the Independence of An Axiom for Temporal Intervals
by Model Generation
Email: zj@ox.ios.ac.cn
Book Announcements
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)