NEWSLETTER

No. 52, August 2001

**Contents**

From the AAR President

Announcement of the 2001 Herbrand Award

A Problem Meriting a Prize

Application of Model Search to Lattice Theory

Properties of Proofs

New Master's Program in Logic and Computation

On-Line Theorem Proving Course Materials Sought

Call for Papers

10th Annual Logic Summer SchoolAAR Membership

Announcement of CADE Elections

New Book

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.

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

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.

Argonne National Laboratory

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

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)) = 1Figure 2: Axioms

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

(*3-M68) x ^ (y V (x ^ (c(x) V (x ^ y)))) = x ^ (c(x) V (x ^ y))

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

(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))))))))

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/`~`

ziegler/qlogic.html,
University of Paderborn, Paderborn, Germany, 1997.

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.

at King's College London

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

- Computational logic
- Knowledge representation and processing
- Algorithm design and analysis
- Modal and temporal logic
- Artificial intelligence
- Logic, reasoning, and action
- Knowledge discovery in databases
- Machine learning
- Agents and multi-agent systems

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.

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**

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.

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.

(Secretary of AAR and CADE)

E-mail: bonacina@cs.uiowa.edu

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:

Year |
AAR Members |

September 1997 | 277 |

September 1998 | 291 |

July 2001 | 553 |

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*

(Secretary of AAR and CADE)

E-mail: bonacina@cs.uiowa.edu

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)

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)

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

Bernhard Gramlich

John R. Harrison

Frank Pfenning

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.

*Automated Theorem Proving in Software Engineering*, by Johann M. Schumann

Foreword by Donald Loveland

Springer Verlag, 2001, XIV+228 pp., ISBN 3-540-67989-8

The growing demand for high quality, safety, and security of software systems can only be met by rigorous application of formal methods during software design. Tools for formal methods in general, however, do not provide a sufficient level of automatic processing. This book methodically investigates the potential of first-order logic automated theorem provers for applications in software engineering.

Illustrated by complete case studies on verification of communication and security protocols and logic-based component reuse, the book characterizes proof tasks to allow an assessment of the prover's capabilities. Necessary techniques and extensions, for example, for handling inductive and modal proof tasks, or for controlling the prover, are covered in detail.

This book demonstrates that state-of-the-art automated theorem provers are capable of automatically handling important tasks during the development of high quality software and it provides many helpful techniques for increasing practical usability of the automated theorem prover for successful applications.

prepared by Gail W. Pieper 2001-09-01