From the AAR President, Larry Wos...
I am astounded and delighted at Maria Paola Bonacina's announcement in this issue of the AAR Newsletter that our AAR membership has increased so dramatically. I remind all of you that your membership entitles you to an impressive reduction in a subscription to the Journal of Automated Reasoning from $267 to only $93, for eight issues. I also encourage you to submit articles, to the journal and to the AAR Newsletter. We welcome challenge problems, applications, and new methodologies, all of which may inspire further advances in the field of automated reasoning.
To set an example, I have included a challenge problem of my own. A warning, though: I too am working on it!
Donald W. Loveland was awarded the Herbrand Award
at IJCAR 2001
for his
contributions to the foundations of automated reasoning,
including the discovery of the model elimination principle,
linear resolution, and near-Horn Prolog.
Loveland's research
opened the way first to Prolog technology theorem proving,
and then to practical tableau-based methods.
Two of Loveland's
papers were also designated as "classics in the field"
in the two-volume book Automation of Reasoning
(Springer-Verlags, 1983),
containing the foundational papers in automated reasoning.
For many, many decades, the worlds of mathematics and logic believed that, to encourage research, Hilbert had in mind twenty-three problems.
After all, in his 1900 Paris lecture, he indeed posed twenty-three problems.
However, quite recently, Rudiger Thiele, through an examination of Hilbert's nachmass, found that Hilbert thought of offering a twenty-fourth problem.
Briefly, that problem focuses on finding simpler proofs.
In that the problem is given in one of Hilbert's notebooks, one can correctly predict that it is not fully presented.
It was not offered, according to Hilbert, because he had not yet formulated it adequately.
However, in a Zurich lecture approximately two decades later, he again discussed the problem.
He also discussed it near the end of his life.
I think it fair to conclude that the problem was close to his heart.
Hilbert was clearly fond of axiomatic proofs, hence the phrase Hilbert-style axiomatic proof.
Such proofs are in fact produced by McCune's automated reasoning program OTTER.
Further--and we now come to the center of this article--OTTER offers various mechanisms that have proved to provide the basis for seeking simpler proofs.
Indeed, whether the simplification (refinement) concerns length, lemma avoidance, term structure, or (indirectly) level or size, methodologies have been formulated that enable a researcher to seek diverse refinements.
This article offers a challenge in the spirit of Hilbert's twenty-fourth problem.
Specifically, you are asked to find a proof of 29 or fewer applications of condensed detachment that shows the fifth of the following five formulas to be dependent on the first four.
With OTTER and the already-cited methodologies, I have found proofs of length 30, some with and some without reliance on double negation.
In fact--and as a maddening example of a veritable snowstorm--I have found twelve proofs of length 30, and I am almost certain I can produce more of that length.
I recently offered the following problem to more than two dozen students in a lecture at Argonne: Find (if one exists) a proof of length less than or equal to 29, using condensed detachment alone.
At the other end of the spectrum, I asked for a proof that the shortest proof of the cited dependence has length 30.
I now offer this problem to AAR Newsletter readers. And as I did for the students,
I offer a monetary prize for the first successful solution.
For an appropriate input file, please see the
Web page.
I note that I first introduced this problem to AAR readers in [Wos1990] and
that, somewhat later,
Maria Paola Bonacina explained the two formulations of the problem
(first-order and equational), provided some historical background,
and gave her solution (with Siva Anantharaman) of the equational formulation in [Bonacina1991]. At that time, the first-order formulation was an open problem;
here, however, the issue is not in finding a proof but in finding the
shortest possible proof.
References
[Bonacina1991] Bonacina, M. P. "Problems in Lukasiewicz
Logic,"
AAR Newsletter No. 18, June 1991.
[Wos1990] Wos, Larry. "New Challenge Problem in Sentential
Calculus," AAR Newsletter No. 16, November 1990.
MACE (Models And Counter Examples)
[3]
and SEM (System for
Enumerating Models) [6]
are programs that search for finite models of
first-order and equational logic statements. If the input statement
is the denial of a conjecture, then any models found are
counterexamples. MACE searches for models by transforming its input
into an equiconsistent propositional problem, then calling a
Davis-Putnam-Loveland-Logeman procedure. SEM uses a more direct
method of filling in tables according to various heuristics and
evaluating the input against the tables. SEM is usually more
effective than MACE for problems with large formulas.
Both programs are designed
to be complete; that is, if the search for a model of size
terminates without finding a model, then there should be none of that
size. We believe the lattices we present in this note are the
smallest ones satisfying the given properties, because the programs
reported that smaller examples do not exist.
This note has a companion page on the
Web that contains
links to MACE, SEM, and EQP input files and other data files related
to this work.
In this note, we refer to those files with bold face.
The standard definition of Boolean algebra is that it is a uniquely
complemented distributive lattice, but other steps along the
way are of interest in the study of quantum logics. As suggested
by Martin Ziegler in [7],
a starting point for
studying the differences between the relatively well understood
classical logic and the less-refined (less-understood) quantum logic,
would be examining the basic underlying structures of each object.
Several such structures are represented as nodes in the hierarchy
shown in Figure 1. Each node represents a variety of lattices defined
by the axioms listed. Each line between two nodes represents an
inclusion of the top class of lattices as a subset of the class
beneath it. The inclusions (B), (D), (E), and (G) are clear from the
axioms alone: in each case, the axioms of the lower class are a subset
of the class above it and hence immediately form a more general
theory. The remaining inclusions (A), (C), and (F) were proved with
the program EQP [1], with inputs available online in files
eqp-a[12].in, eqp-c.in, and eqp-f.in,
Figure 1: Structure Hierarchy
Using these equations, MACE and SEM found models that prove that
none of the axiom sets for the separate types of lattice are
equivalent. This was accomplished by supplying the axioms for a given
type of lattice along with the negation of another axiom or set of
axioms which are unique to the second type of lattice. The diagrams
in Figure 3 are labeled to correspond to their use in Figure 1.
Figure 3: Lattices
For example, in order to obtain the model (A) that satisfies all the
axioms of a modular ortholattice but is not necessarily a Boolean
algebra, the axioms (1), (2), (3), (5), (6), and (7) are included as
input while axiom (4) is denied. MACE then searched to find a model
that satisfies all the input clauses including the denial. A matrix
of values explicitly listing the operation values for meet, join and
complement was returned that translated to model (A). The MACE
inputs for models (A), (B), (C), (D), and (F), are available online in
files mace-[abcdf].in.
The procedure used to find models (E) and (G) was different because
we must find a lattice (or modular lattice) without an appropriate
complement operation. We did this in two stages: first finding
a lattice (or modular lattice) satisfying invertibility but not
compatibility, then showing that that particular lattice does not
have a complement operation. In the case of (E), for example,
axioms (5) and (6), which distinguish ortholattice theory from
lattice theory, introduce complementation. With axioms
(1), (2), (3), and (5) with the denial of (6), MACE's output gave a
model that included a list of values defining the complement
operation c(x). From the output we know that the operation
explicitly found by MACE does not satisfy the ortholattice axioms;
however, we need to prove that no possible complement exists for
the lattice that could satisfy the additional axioms of an
ortholattice. The function values found in the candidate lattice were
inserted into the input, forcing MACE to consider the same lattice but
now with the axioms of an ortholattice included (5) and (6) in their
original form (not negated). A second search with this input allowed
all possible functions c(x) under axioms (5) and (6) to be considered.
The search was complete with no models found, proving that the
candidate lattice indeed cannot be an ortholattice.
The MACE inputs for models (E) and (G) can be found online in
files mace-e[12].in and mace-g[12].in.
In 1999, Megill asked [4] whether the equation
holds in all weakly orthomodular lattices. SEM found a
countermodel of size 20, which is depicted in Figure 4.
Figure 4: RW-1
This lattice (named RW-1) answers an open question published by Megill
and Pavicic in [5, eq. 2.12]
and several of Megill's
unpublished questions [4].
The SEM input
that produced this lattice is available online in file
sem-rw-1.in.
In July 2001, Megill asked us [4]
whether
the equation
holds in every ortholattice. SEM found a countermodel of size 16,
shown in Figure 5.
The SEM input can be found online in file sem-rw-2.in.
Figure 5: RW-2
We thank Bill McCune, who supervised our work at Argonne during the summer of
2001 and who suggested the problems to us.
This work was supported by
the Mathematical, Information, and
Computational Sciences Division subprogram of the Office of Advanced
Scientific Computing Research, U.S. Department of Energy, under
Contract W-31-109-Eng-38 and by the Department of Educational Programs,
Argonne National Laboratory.
1. W. McCune.
33 basic test problems: A practical evaluation of some paramodulation
strategies.
In Robert Veroff, editor, Automated Reasoning and its
Applications: Essays in Honor of Larry Wos, chapter 5, pages 71-114.
MIT
Press, 1997.
2. W. McCune.
Automatic proofs and counterexamples for some ortholattice
identities.
Information Processing Letters, 65:285-291, 1998.
3. W. McCune.
MACE 2.0 Reference Manual and Guide.
Tech. Memo ANL/MCS-TM-249, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, June 2001.
4. N. Megill.
Correspondence with W. McCune by electronic mail, 1997-2001.
5. N. Megill and M. Pavicic.
Equations and state and lattice properties that hold in infinite
dimensional Hilbert space.
International J. Theoretical Physics, 39:2337-2379, 2000.
6. J. Zhang and H. Zhang.
SEM: A system for enumerating models.
In Proceedings of the International Joint Conference on
Artificial Intelligence. Morgan Kaufmann, 1995.
7. M. Ziegler.
Quantum logic: Order structures in quantum mechanics.
http://lagrange.uni-paderborn.de/
Many researchers are content to know that some claim has been proved, that a statement has been shown to be a theorem.
Others--certainly including me--are interested in (or preoccupied with) the explicit presentation of a proof.
Indeed, sometimes the very properties of a proof fascinate me.
This article focuses on one such property.
To gain a taste of proof properties, consider what can be termed compact proofs.
A proof is compact if and only if (1) it is a proof of a conjunction of two or more formulas or equations and (2) it is in fact a proof of one of the members of the conjunction.
For example, with OTTER, I have found compact proofs that deduce the Church three-axiom system from the Lukasiewicz three-axiom system for two-valued sentential (or propositional calculus).
Specifically, the proofs are of length 21 and are precisely a proof of thesis 35, where the system consists of theses 18, 35, and 49.
In other words, the proofs of 18 and 49 are properly contained in the proof of 35, which is indeed therefore a proof of the conjunction.
A second property of a proof that can occupy my attention, especially because it offers an obvious obstacle for discovery by an automated reasoning program, is the presence of a sequence of steps three or more in length, each of which is far more complex than the rest of the proof.
Ordinarily, even if the first of the three steps is deduced, the program will not focus readily on that step to then deduce the next step, in turn chosen as the focus to deduce the third.
Such high and somewhat wide plateaus make the life of one using a reasoning program most trying.
We now come to the property of concern here.
The property can be viewed as geographic or topological.
In a sense, the type of proof in question has within it an island, with the rest of the proof moving up to the end of the island and resuming only when the island has been traversed.
In a different sense the proof "splits".
A double-negation term is a term of the form for some term .
A formula is a double-negation formula if it contains such a term.
In particular, I have in hand a 62-step proof of a distributive law in infinite-valued sentential calculus whose steps can be rearranged such that the first fifty are free of double-negation terms, the next ten rely on double negation, and the last two do not.
Double negation is not needed in this rearrangement for a long while; then it appears and occupies the entire stage; then it disappears.
The proof "splits" into a double-negation-free part and a part demanding double negation.
Obviously, the two parts are connected, but barely.
A natural question to ask is why properties such as these are of such concern to me.
Put another way, what do I hope to gain by looking at the properties of a proof rather than examining the search space?
The answer rests with my intuition that if we could classify proofs by their properties (for example, level, size, purity, compactness), we might discover how to obtain better proofs.
I therefore plan to continue this discussion of proof topology in subsequent issues of the AAR Newsletter; and I welcome comments and contributions from readers.
Starting in September 2001, the Department of Computer
Science at King's College London is offering a new
MSc program in Logic and Computation. This one-year
postgraduate course is designed to provide skills essential
for the solid understanding of the fundamentals of logic
and its potential use in the solution of complex
computational problems, such as the representation of
knowledge, planning, the design of intelligent agents,
natural language understanding, and automated reasoning.
The MSc in Logic and Computation will build sound
theoretical foundations exploiting the Department's
research strengths in the area and is closely linked to the
internationally renowned group of logic and computation
led by Dov Gabbay. Courses in the MSc program will be
taught by David Makinson, Andrew Jones,
Michael Zakharyaschev, Agnes Kurucz, and Odinaldo Rodrigues
(among others).
The program includes course units such as
For further information on the program and the application
procedure, please visit the
Web page.
For further information on the Group of Logic and
Computation at King's College, see
the
Web page.
I am preparing a
Web page
of links to
on-line teaching materials for courses in automated theorem proving.
The purpose of this page is to facilitate the teaching of courses in
theorem proving by providing course notes, transparencies, handouts,
and assignments online for use in course preparation.
Please send
URLs of such material, along with a general description of its
nature, to
plaisted@cs.unc.edu
The subject areas covered include
propositional, first-order, and higher-order theorem proving,
classical and nonclassical logics, resolution and nonresolution
methods, and mathematical induction. Courses in logic per se
are not sought, but rather courses emphasizing automated deduction.
Methods for Modalities
The workshop Methods for Modalities (M4M) aims to bring together
researchers interested in developing proof tools and reasoning methods for
modal logic. M4M will be centered
on a number of long presentations by leading researchers; these
presentations aim to provide both the general background and inside
information in a number of key areas. To complement these, the organizers
invite submissions of short (up to 10 pages) presentations aimed at highlighting
new
developments and applications; submissions of system demonstrations
(up to 4 pages); and application descriptions (up to 6 pages).
Submissions should be sent by October 12, 2001, to m4m@science.uva.nl.
For further information, see the
Web site.
2nd International Workshop on Implementation of Logics
The second
Reunion Workshop on Implementations of Logic will be
held in conjunction
with the 8th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning, LPAR'2001, in Havana, Cuba,
December 3-7, 2001.
The organizers are seeking contributions describing the implementation of
automated reasoning programs, theorem provers for various logics,
logic programming systems, and related technologies. Topics of
interest include the following:
Of particular interest are in contributions that help the
community to understand how to build useful and powerful reasoning
systems.
Four-page abstracts should be submitted by September 15, 2001.
For further details about the workshop, including the submission
process, please consult the
Web page.
CICLOPS 2001
A colloquium on
"Implementation of Constraint and LOgic Programming Systems"
will be
held in conjunction with the
International Conference on Logic Programming
at Paphos, Cyprus, on December 1, 2001.
This year's event also will join
forces with TRICS (Techniques for Implementing Constraint Programming
Systems),
thus providing coverage
to implementation technology for both logic and constraint programming.
The past several years have seen continuous progress in the computing technology
available for the academic and the commercial computing environments.
Examples include improved processor performance, increased memory capacity
and bandwidth, faster networking technology, and operating system support for
cluster computing. Combined with recent advances in compilation
technologies, these improvements are causing high-level languages to be
regarded as good candidates for programming complex, real world
applications.
Logic programming and constraint programming, in particular, seem to offer
one of the best alternatives, as they couple a very high level of
abstraction and a declarative nature with an extreme flexibility in the
design of its execution model.
The main intent of this workshop is to bring together, in an informal
and friendly setting, key researchers on implementation technologies
for logic and constraint-based languages and systems, in order to promote
a much needed exchange of ideas and feedback on recent developments.
The workshop is focused on design and implementation of logic and
constraint programming systems whether sequential, parallel,
or concurrent. Preference will be given to the analysis and description
of implemented systems (or systems currently under implementation) and
their associated techniques, problems found in their development or
design, and steps taken towards the solution of these problems.
Suggested topics of interest include
Authors are invited to submit papers
(not exceeding 12 pages)
in Postscript or PDF form by electronic
mail by September 5, 2001, to the workshop coordinator
Enrico Pontelli,
email: epontell@cs.nmsu.edu.
For further information, see the
workshop
Web site.
The Australian
National University will be hosting the 10th Annual Logic Summer
School. The school will consist of short courses on aspects of pure
and applied logic taught by experts from Australia and overseas.
The school will be held December 3-14, 2001, and is suitable
for IT professionals using formal methods or problem-solving
technologies, teachers who teach logic, students who are going on to
do research in logic or a related fields, whether in computing,
mathematics or philosophy.
The cost of the school is $1,650/person (GST inclusive). Discounts
may be negotiated for companies or institutions that send more than
one participant to the school. Students in full-time education are
eligible for a reduced fee of $120/person (GST inclusive). For
information on scholarships for students please see the
Web site.
The closing date for early registration is November 2, 2001.
Registrations received after this date will be subject to 20%
surcharge.
If you would like additional information about this course please
contact The Automated Reasoning Group
at lss-admin@arp.anu.edu.au or phone 61 (02) 6125 8630.
As of July 6, 2001, the Association for Automated Reasoning has
over 500 members, for the first time in its history.
The following table summarizes recent membership levels:
The growth from September 1997 through September 1998
was due in part to the CADE-15 conference (Lindau, July 1998),
which had 191 participants,
while CADE-16 (Trento, Italy, within FLoC, June 1999),
with 148 participants,
CADE-17 (Pittsburgh, U.S.A, June 2000) with 106 participants,
and especially IJCAR 2001 (Siena, Italy, June 2001),
with 250 participants, determined to a large extent
the growth from September 1998 through July 2001,
reaching and passing the 500 threshold.
The list of members is available on the Web,
reachable from the AAR home page, and directly at
the
Web site.
All members are encouraged to consult this list
and send by e-mail corrections and additions,
especially the URL of their home page, if missing.
The list of members on the Web will be updated at least once per
year, as time permits.
Maria Paola Bonacina
An election of CADE trustees will be held soon
and all AAR members will receive a ballot.
The following people are currently serving as Trustees of CADE Inc.:
Maria Paola Bonacina (Secretary)
The terms of office of Claude Kirchner and Frank Pfenning are expiring,
because CADE trustees are elected to serve for three years,
as well as that of Tobias Nipkow.
The position of Tobias Nipkow is replaced by Andrei Voronkov,
as CADE 2002 Program Chair.
Nonetheless, there are three positions to fill, because
CADE Inc. is implementing the amendment to its bylaws,
approved by the membership in the summer of 2000,
that requires to increase the number of trustees from nine to twelve,
by electing three trustees instead of two for three elections.
The first election with an additional slot was held last year,
and this is the second such election
(see AAR Newsletter No. 48, August 2000).
The following candidates were nominated:
Gilles Dowek
and provided the following statements.
Statement by Gilles Dowek
My first wish for the Automated Reasoning Community is that its
different parts continue to talk to each other. In particular, I
support efforts like the last IJCAR conference. This conference was a
big success because it was an ``agora'' where people could talk, listen,
learn and meet. A large PC and many workshops and tutorials have
permitted to avoid the concentration of power into too few hands. In
the same spirit, I have participated to the Robinson and Voronkov
Handbook. I consider that such efforts that permit to popularize
recent results are important.
My second wish is that the community can talk to other communities. In
my own work, I have been interested in the cross fertilization of
proof theory and automated reasoning. I consider that the ideas
coming from lambda-calculus, proof theory, calculability and model
theory are not always enough popularized in our community. In the same
way, I consider that there is no real border between automated
reasoning systems and proof cheking systems. Many applications of
automated reasoning can be found in the domain of proof checker
design, as well as computer algebra.
If I happen to be elected as a trustee, I will try to act in these
directions.
Statement by Bernhard Gramlich
For a long time, CADE is one of the major scientific forums for my
research interests and activities. Since 1997 I have co-organized the
workshop on Strategies in Automated Deduction yearly (with a break in
2000) in conjunction with CADE. My other main research interests in
CADE are rewrite-based deduction and inductive theorem proving.
As to the policy of and perspectives for CADE, both as community and
as organization, I think that we should, in particular,
In case of being elected as CADE trustee, I would try to promote these
ideas.
Statement by John Harrison
There is currently a schism in automated reasoning between the
"automatic" and "interactive" camps, and not enough communication
between them, still less an effective combination of their
respective strengths in new and more powerful theorem proving
systems. While the "automatic" approach still dominates research
and teaching, and has led to most of the interesting conceptual
advances, it is the "interactive" approach that has proved
successful in formalizing large bodies of mathematics and meeting
the needs of practical applications. Both camps have much to
learn from each other, e.g.
I think that CADE and IJCAR are the natural place for people
interested in all aspects of computer-aided theorem proving
to meet and learn from each other, and I hope to see the
interpretation of "automated" in the names CADE and IJCAR
continue to broaden.
Statement by Frank Pfenning
If re-elected, I plan to continue my current work
on behalf of the automated reasoning community. I believe
organzing and promoting our conferences and workshops
are the most important tasks for a CADE trustee, and
I have contributed accordingly by chairing
CADE-17 in Pittsburgh, through participation in the IJCAR
steering committee, and by serving on the program
committees of several workshops and related conferences
such as LPAR and TPHOLs. I also think more could and should be done
within our community to reach out and interact
with related areas such as the hardware and
software verification, databases, and programming languages.
I have established some connections through my research,
and I also submitted an ultimately unsuccessful proposal
to co-locate TPHOLs with IJCAR in Siena. I hope that
IJCAR can become a regular event every two or three years
and that we can broaden its scope through occasional co-location
of related conferences, thereby raising the awareness of
automated deduction techniques in other fields and in turn
showing us which practical or theoretical problems of
potential consumers of our methods deserve our attention.
Announcement of the 2001 Herbrand Award
A Problem Meriting a Prize
Larry Wos
P(i(x,i(y,x))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(i(x,y),y),i(i(y,x),x))).
P(i(i(n(x),n(y)),i(y,x))).
P(i(i(i(x,y),i(y,x)),i(y,x))).
These five formulas (in which the functions and , respectively, denote implication and negation) were originally presented as an axiom system for infinite-valued sentential calculus by Lukasiewicz.
C. A. Meredith showed some years later that the fifth is in fact dependent.
Meredith's proof is roughly of length 37, relying on the use of what can be termed double-negation formulas, formulas in which
n(n(t))
for some term t occurs.
Application of Model Search to Lattice Theory
Michael Rose and Kristin Wilkinson
Argonne National Laboratory
1. Introduction
We have used the first-order model-searching programs MACE and SEM to
study various problems in lattice theory. First, we present a case
study in which the two programs are used to examine the differences
between the stages along the way from lattice theory to Boolean
algebra. Second, we answer several questions posed by Norman Megill
and Mladen Pavicic on ortholattices and orthomodular
lattices. The questions from Megill and Pavicic arose in
their study of quantum logics, which are being investigated in
connection with proposed computing devices based on quantum mechanics.
Previous questions of a similar nature were answered by McCune and MACE
in [2].
2. From Lattice Theory to Boolean Algebra
Commutativity (1)
x ^ y = y ^ x
x V y = y V x
Associativity (2)
(x ^ y) ^ z = x ^ (y ^ z)
(x V y) V z = x V (y V z)
Absorption (3)
(z V y) ^ x = x
(x ^ y) V x = x
Distributivity (4)
x ^ (y V z) = (x ^ y) V (x ^ z)
Invertibility (5)
x V c(x) = 1
x ^ c(x) = 0
c(c(x)) = x
Compatibility (6)
c(x V y) = c(x) ^ c(y)
c(x ^ y) = c(x) V c(y)
Modularity (7)
x V (y ^ (x V z)) = (x V y) ^ (x V z)
Orthomodularity (8)
x V (c(x) ^ (x V y)) = x V y
Weak Invertibility (9)
x V c(x) = 1
c(c(x)) = x
Weak Orthomodularity (10)
(c(x) ^ (x V y)) V (c(y) V (x ^ y)) = 1
Figure 2: Axioms
3. Answers to Two Questions
(*3-M68) x ^ (y V (x ^ (c(x) V (x ^ y)))) = x ^ (c(x) V (x ^ y))
(4) (x V (c(y) ^ (c(x) V (c(y) ^M (x V (c(y) ^M c(x))))))) =
(x V (c(y) ^ (c(x) V (c(y) ^ (x V (c(y) ^ (c(x) V (c(y) ^ x))))))))
Acknowledgments
References
~ziegler/qlogic.html,
University of Paderborn, Paderborn, Germany, 1997.
Properties of Proofs
Larry Wos
New Master's Program in Logic and Computation
at King's College London
On-Line Theorem Proving Course Materials Sought
David A. Plaisted
Call for Papers
10th Annual Logic Summer School
AAR Membership Tops 500
Maria Paola Bonacina
(Secretary of AAR and CADE)
E-mail: bonacina@cs.uiowa.edu
Year
AAR Members
September 1997
277
September 1998
291
July 2001
553
Announcement of CADE Elections
(Secretary of AAR and CADE)
E-mail: bonacina@cs.uiowa.edu
Ulrich Furbach, President (elected 10/2000)
Harald Ganzinger (past Program Chair, elected 10/1999)
Claude Kirchner (past Program Co-chair, elected 10/1998)
Michael Kohlhase (elected 10/2000)
David McAllester (past Program Chair, elected 10/2000)
Neil V. Murray (Treasurer)
Tobias Nipkow (IJCAR 2001 Program Co-Chair)
Frank Pfenning, Vice-President (elected 10/1998)
David A. Plaisted (elected 10/1999)
Andrei Voronkov (CADE 2002 Program Chair)
Bernhard Gramlich
John R. Harrison
Frank Pfenning