AARNEWS - August 2001

ASSOCIATION FOR AUTOMATED REASONING

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

  • Methods for Modalities
  • 2nd International Workshop on Implementation of Logics
  • CICLOPS 2001
  • 10th Annual Logic Summer School
    AAR Membership
    Announcement of CADE Elections
    New Book

    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!

    Announcement of the 2001 Herbrand Award

    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.

    A Problem Meriting a Prize


    Larry Wos

    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 n(n(t)) for some term t occurs.

    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.

    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].

    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.

    2. From Lattice Theory to Boolean Algebra

    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

    The focus of this section is on proving these inclusions to be strict inclusions by finding explicit models. An explicit model can add to an intuitive description of the theories involved. For example, each model given below resulted only after several earlier completed exhaustive searches, and so each model given is the smallest model that exists for the particular problem. Each node in Figure 1 represents a class of lattices that satisfy the axioms listed in Figure 2.

    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

    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.

    3. Answers to Two Questions

    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

    Acknowledgments

    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.

    References

    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.

    Properties of Proofs

    Larry Wos

    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.

    New Master's Program in Logic and Computation
    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

    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.

    On-Line Theorem Proving Course Materials Sought

    David A. Plaisted

    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.

    Call for Papers

    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.

    10th Annual Logic Summer School

    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.

    AAR Membership Tops 500

    Maria Paola Bonacina
    (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.

    Announcement of CADE Elections

    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,

  • increase efforts to bridge the gap between theory and applications,
  • encourage subfields where major progress seems important (which include among others strategies and induction),
  • clarify the relation to neighbouring fields, communities and conferences (like CAV, TPHOLs, FME, ...) in order to regain former strength, and
  • continue with the IJCAR experiment that has turned out to be very successful and promising this year in Siena, every 2 or 3 years.
  • 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.

  • Many interactive provers require tedious user guidance to solve problems that can trivially be dealt with automatically by more powerful automated theorem provers. Developers of interactive theorem provers need to become aware of how powerful these techniques are, and study the difficulties involved in integrating them into interactive provers without compromising logical soundness.
  • The problems traditionally used as benchmarks for automated theorem proving are often quite clean statements from pure mathematics (prove that a ring in which $x^3 = x$ is commutative, etc.). However, many of the problems arising in practice have a different flavor, and it may well be that the consensus on the value of certain features will shift significantly in the light of ``real world'' problems.
  • 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.

    New Book

    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