No. 50, February 2001


From the AAR President
Three $1 Challenge Problems
Millennium Prize Problems and Millennium Lectures
Herbrand Award: Call for Nominations
Call for Papers

  • WRS 2001
  • Workshop on Theory and Applications of Satisfiability Testing
  • Workshop UNIF 2001
  • Workshop STRATEGIES 2001
  • Workshop Mathematical Induction
  • Workshop Future Directions in Automated Reasoning
  • Workshop on Inconsistency in Data and Knowledge
  • TPHOLs 2001
  • CHARME 2001
  • LPNMR'01
  • KI-2001
  • ASCM 2001

  • New Book on Automated Reasoning with Otter

    From the AAR President, Larry Wos...

    I find it piquant that, as Bob Boyer has informed me, there now exist million dollar prizes in mathematics; see the announcement in this newsletter about the related lecture series at the University of Texas. Just as Hilbert's posing of twenty-three problems motivated significant new research, so too may these prizes direct the field and lead to extremely interesting results in mathematical analysis.

    Of course, I would find it most interesting if our AAR readers would come up with a similar set of challenging problems to stimulate and direct research in automated reasoning. The problems I posed in the book 33 Basic Research Problems were one attempt at challenging researchers. Newer problems were posed in Chapter 11 of A Fascinating Country in the World of Computing; its CD-ROM contains the out-of-print book 33 Basic Research Problems. On a smaller scale, I now issue a challenge to each AAR member: Submit to me one problem or open question that might be profitably attacked by an automated reasoning system. I will collect these in a library and publish them for all our readers to attack. No, I am not offering a million dollars--to submitters or to solvers. Fame and glory might result. I am certain that many find sheer delight in solving an interesting problem and find the research worthwhile.

    To provide impetus, I include in this issue three problems. They are not open questions, but I think AAR readers may find them challenging.

    Three $1 Challenge Problems

    Larry Wos, Argonne National Laboratory (

    Being of sound mind and reasonable wallet, I offer here three $1 automated reasoning problems, in the spirit of the $1 million mathematics problems recently announced in Paris.

    1. MB24

    The first of our challenge problems involves the following three axioms L1, L2, and L3 of Lukasiewicz for two-valued sentential (propositional) calculus.

    The problem asks one to produce a double-negation-free proof--one that is free of n(n(n(r)), where the function n denotes negation and r is any term--that relies solely on the inference rule condensed detachment and deduces the specific formula t, where t is the following.
    The proof must be obtained by using an automated reasoning program.

    It is known that this area of logic is D-complete; that is, any tautology (theorem) is deducible with condensed detachment. What is not known is whether one can always obtain a double-negation-free proof. Nor does D-completeness tell us how to obtain a condensed detachment proof.

    Note, moreover, that the wording of the challenge here is precise: It is not sufficient to produce a proof of a more general theorem; indeed, OTTER can do this easily in the presence of forward subsumption. But subsumption gets in the way of finding the specific result.

    Our success involved several steps. First, Dolph Ulrich provided a proof by hand of the specific theorem, assuming the provability of two key lemmas. Next, Brandon Fitelson took Ulrich's proof and, using a special version of OTTER developed by Robert Veroff, obtained a proof. Then, I took Fitelson's proof and, with several tricks, found a means for the publicly available OTTER to derive the desired proof.

    Specifically, to avoid having OTTER subsume t, I had OTTER demodulate t to a constant (OTTER performs demodulation before it performs subsumption). I then put the not of that constant in the passive list, took other actions, and--success! Most recently we found a proof of length 25 (applications of condensed detachment) and level 16.

    I invite AAR readers to find a more elegant (shorter) proof with OTTER or another automated reasoning program.

    2. MB23

    Similar to the preceding problem, MB23 begins with the three Lukasiewicz axioms and asks for a condensed-detachment, double-negation-free proof, though of course of a different lemma, the following.

    This problem is significantly harder than MB24, however. Indeed, one might regard it as presenting a "nested" version of the obstacles presented by MB24. Specifically, in the proof we have for this problem, three or four formulas must be proved, each of which is subsumed by a clause along the way.

    Bob Veroff has solved this problem using his special version of OTTER that includes a more general treatment of the hints strategy [Veroff1996]. The length of the proof is 34; the level of proof is 17. To date, however, no proof has yet been obtained by using the standard arsenal offered by OTTER. I continue to work on the problem; perhaps one of our readers, using OTTER, will beat me to the solution--and win the $1.

    3. Commutator Problem

    The following problem was provided by Michael Beeson. It is taken from a homework assignment given in an algebra course at MIT.

    Problem: Prove the commutator subgroup of a group is normal.

    To formulate the problem more symbolically:

    Write a* for a-inverse. Define [a,b] =3D aa*bb*. Then prove x*[a,b]x has the form [u,v] for some u and v.

    The proof is but one line, if produced by a person with intuition. Indeed, this is the type of problem a mathematician can solve quickly. The challenge, however, lies in getting a computer program to come up with the right choice for u and v.

    Consider the following "baby" example: If in a group x times x is the identity e, then the group is commutative.

    A person will probably begin to solve such a problem with the simple deduction "Then yz times yz equals e ." But OTTER cannot make this deduction, not offering instantiation. Indeed, if it did, the result would be subsumed. And if one turned off subsumption, the result would be disaster: a combinatorial explosion.

    I find such baby problems fascinating because they illustrate the remarkable difference between the approach taken by an unaided person and that taken by a reasoning program.

    I offer Beeson's problem (not the "baby" example) as a challenge to our readers; with appropriate choices, OTTER finds a solution very, very quickly.


    [Veroff1996] Veroff, R., "Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies" J. Automated Reasoning 16, no. 3 (1996) 223-239.

    Millennium Prize Problems and Millennium Lectures

    Robert Boyer (

    In May 2000, at the College de France in Paris, the Clay Mathematics Institute of Cambridge Massachusetts (CMI) announced seven Millennium Prize Problems, designating a $7 million prize fund for the solution to these problems, with $1 million allocated to each.

    The Department of Mathematics at the University of Texas is pleased to announce a series of seven general audience evening lectures, "The Millennium Lectures," based on the "Millennium Prize Problems." The aim is to explain to a wide audience the historical background of these problems, why they have resisted many years of serious attempts to solve them, and the roles these problems play in modern mathematics.

    The lecture series will run throughout the Spring Semester 2001 on the campus of the University of Texas at Austin and will be given by members of Departments of Mathematics and Computer Sciences. Each lecture will be introduced by Professor John Tate, who helped announce the "Millennium Prize Problems" and will be followed a reception.

    February 7: The Poincare Conjecture -- Cameron Gordon
    February 21: The Birch and Swinnerton-Dyer Conjecture -- Fernando Rodriguez-Villegas
    March 7 : Yang-Mills Existence and Mass Gap -- Lorenzo Sadun
    March 28 : P versus NP -- Vijaya Ramachandran
    April 11 : Navier-Stokes Existence and Smoothness -- Luis Caffarelli
    April 25 : The Hodge Conjecture -- Dan Freed
    May 2: The Riemann Hypothesis -- Jeff Vaaler

    Lectures will take place at 7:00 pm in TCC 1.110 in the Thompson Conference Center. For further information contact Alan Reid, by e-mail, or by phone (512) 471 3153. See also the Web site.

    Herbrand Award: Call for Nominations

    Maria Paola Bonacina
    Secretary of AAR and CADE
    On behalf of the CADE Inc. Board of Trustees

    The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

    Larry Wos (1992)
    Woody Bledsoe (1994)
    Alan Robinson (1996)
    Wu Wen-Tsun (1997)
    Gerard Huet (1998)
    Robert S. Boyer and J Strother Moore (1999)
    William W. McCune (2000).

    A nomination is required for consideration for the Herbrand award. Nominations can be made at any time and remain open indefinitely, but only nominations received by March 15, 2001 will be considered for a Herbrand Award at IJCAR in June 2001.

    Nominations should consist of a letter (preferably email) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to Ulrich Furbach, President of CADE Inc.,, with copies to

    Call for Papers

    WRS 2001

    An international Workshop on Reduction Strategies (WRS 2001) in rewriting and programming will be held in conjunction with RTA 2001 at Utrecht, The Netherlands, May 26, 2001.

    Reduction strategies in rewriting and programming have attracted increasing attention within the past years. New types of reduction strategies have been invented and investigated, and new results on rewriting/computation under particular strategies have been obtained. The need for a deeper understanding of reduction strategies in rewriting and programming, both in theory and practice, is obvious, since they bridge the gap between unrestricted general rewriting (computation) and (more deterministic) rewriting with particular strategies (programming). Moreover, reduction strategies provide a natural way to go from operational principles and semantics to implementations of programming languages. Therefore, progress in this area is likely to be of interest not only to the rewriting community but also to neighboring fields such as functional programming, functional-logic programming, and termination proofs of algorithms.

    WRS 2001 seeks to provide a forum for presenting and discussing new ideas and results, recent developments and new research directions, as well as of surveys on existing knowledge in this area. Especially welcome are interactions between researchers and students actively working on such topics.

    Topics of interest include theoretical foundations for the definition and semantic description of reduction strategies; strategies in different frameworks; properties of reduction strategies/computations under strategies; interrelations, combinations, and applications of reduction under different strategies; program analysis and other semantics-based optimization techniques dealing with reduction strategies; rewrite systems, tools, and implementations with flexible programmable strategies; specification of reduction strategies in (real) languages; and data structures and implementation techniques for reduction strategies.

    Research paper submissions (up to 10 pages) should describe unpublished work; survey papers may be longer than 10 pages. Submissions should be sent in postscript format to the PC co-chairs ( by March 1, 2001. Accepted papers will be included in the workshop proceedings that will be available at the workshop and electronically on the Web.

    Researchers interested in attending the workshop may send a email to by March 1, 2001, preferably together with a brief position paper (up to two pages in postscript) describing their interest or work in the area.

    For further information, see the Web site.

    LICS 2001 Workshop on "Theory and Applications of Satisfiability Testing"

    Great strides have been made in recent years in the theory and practice of propositional satisfiability testing. On the theoretical side, a wide range of mathematical approaches--ranging from classical combinatorial analysis to arguments based on statistical physics--have increased our understanding of problem hardness. On the practical side, new systematic and non-systematic search algorithms have increased the size of problems that can be solved by several orders of magnitude. As a result there is an growing interest in using SAT as a practical tool for solving real-world problems, as well as using the insights gained from SAT research to create problem-specific solutions.

    The purpose of this workshop is to bring together researchers from different communities--including theory, artificial intelligence, verification, mathematical theorem-proving, and operations research--in order to share ideas and increase synergy between theoretical and empirical work. The workshop will take place in Boston on June 14-15, 2001.

    Invited speakers are Alasdair Urquhart (University of Toronto), Daniel Jackson (MIT), and Michael Littman (AT&T Laboratories).

    The deadline for submission of papers (max. 8 pages) is March 15, 2001. In order to increase time for free discussion, some authors may be asked to give short (10-minute) overviews of their work rather than a full talk. All accepted papers will appear in an online set of working notes.

    Those who wish to participate in the workshop but not submit a paper should send an email to by March 15 with relevant contact information.

    For more information about the workshop see the Web page or email Henry Kautz

    IJCAR Workshop "UNIF 2001"

    The fifteenth international workshop on unification will take place June 18-19, 2001, in Siena, Italy. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers.

    The main purpose of UNIF is to bring together people interested in unification, to present recent (even unfinished) work, and to discuss new ideas and trends in unification and related fields. In particular, it offers a good opportunity for young researchers and researchers working in related areas to get an overview of the state of the art in unification theory and to contact experts in the field.

    Topics of interest include the following: general e-unification and calculi, special unification algorithms, matching, narrowing, higher-order unification, combination problems, disunification, typed unification, constraint solving, unification calculi, applications, implementations, type checking and reconstruction, unification-based approaches to grammar, and applications.

    Those interested in participating to UNIF 2001 should send email to by April 15, 2001. Those interested in giving a talk should also submit an extended abstract (2-4 pages, including a postscript version and the Latex2e source file) and specify whether the talk will be a short (15-minute) or a long (30-minute) one.

    For further information, see the UNIF 2001 Web site.

    IJCAR Workshop "STRATEGIES 2001"

    Strategies are almost ubiquitous in automated deduction and reasoning systems, yet only recently have they been studied in their own right. STRATEGIES 2001 aims at making progress toward a deeper understanding of the nature of strategies and search plans, their description, properties, and usage, especially, but not exclusively, in theorem proving and model building.

    Topics of special interest for the workshop are (1) theory and analysis of strategies (e.g., formal approaches for abstract representation and comparison of theorem proving strategies and their behavior, terminological foundations); (2) strategies in (existing) theorem proving systems (e.g., representation and implementation of the proof search model, integration of strategies into this model, flexibility, programmability, transparency, role of the user); (3) strategy languages (e.g., adequacy for certain purposes, theoretical foundations, practical usefulness, comparison with other approaches, applications); and (4) applications and case studies in which strategies play a major role.

    Attendance at the workshop is be invitation only. Authors interested in presenting their work related to strategies are invited to submit an extended abstract of up to 10 pages. Researchers interested in attending the workshop without giving a talk may send a position paper of 1-2 pages describing their interest in the mentioned topics. All submissions should be sent to the Program Chairs ( in Postscript before March 31, 2001.

    For further information, please see the Web site.

    IJCAR Workshop on "Mathematical Induction"

    Mathematical induction is required for reasoning about objects or events containing repetition, for example, computer programs with recursion or iteration, electronic circuits with feedback loops, or parameterized components. Induction is thus a vital ingredient of formal methods techniques for synthesizing, verifying, and transforming software and hardware. The automation of induction proof improves the capability of mechanical assistants for software and hardware designers. It reduces the need for such designers to be skilled in mathematical proof techniques and improves their productivity by automating tedious and error-prone aspects to their task in a formal software development.

    This one-day workshop will focus on mathematical induction, with sessions on such areas as the combination of inductive theorem provers with decision procedures and other reasoning components, program synthesis and transformation, and the use of induction in logical frameworks. Researchers interested in attending the workshop are asked to submit ashort abstract or a position paper describing their current research in the area or a system description of some relevant implementation work they have performed. The submission deadline is March 31, 2001. For details, see the Web site.

    IJCAR Workshop "Future Directions in Automated Reasoning"

    Automated reasoning systems have formed the core of many AI software systems since the formation of the field. The efficiency of the systems has significantly improved markedly: very hard problems that were out of scope a few years ago can now be solved either fully automatically or in an interactive way. However, more than 40 years after the foundation of the field and at least 30 years after the formulation of the dream to build artificial mathematical assistants, it is still in many ways frustrating to use automated reasoning systems. This workshop will look at what is missing in state-of-the-art systems and which developments would be most beneficial for the field. Of particular interest are challenge examples together with an analysis why they are difficult for current systems and how they may be solved in the future.

    Topics of interest include interaction vs automation, proof planning,making more use of second and higher-order representations and unification, a multi-agent approach to reasoning, combining the best features of different systems, improved algorithms for finding proofs by induction, creating and utilizing databases of proved results, concept formation, model-based reasoning, machine-learning approaches, multiple representations and re-representations of problems and reasons, and connections between calculation and logical reasoning.

    Potential participants should either submit a short statement (up to 2 pages) describing their current interests or, if they wish to make a short (up to 5 pages) or long (up to 15 pages) presentation, an abstract of the work they want to present. Submissions should be sent to Manfred Kerber at

    For further information, see the Web site.

    IJCAI Workshop on "Inconsistency in Data and Knowledge"

    The problem of reasoning in the presence of inconsistency has been studied by the mathematical logic community for some decades. Nevertheless, new challenges, problems, and issues have appeared in the context of knowledge representation in AI, database systems, formal specifications, and other areas of computer science. The main goal of this workshop, then, is to identify new inconsistency-related problems of conceptual and practical significance and the ways they are handled in different contexts. The workshop will take place on August 6, 2001. It is expected to bring together people from different research communities (knowledge representation, databases, formal specifications, mathematical and philosophical logic) that are actively pursuing the issue of inconsistency.

    Topics of interest include reasoning in the presence of inconsistency, inconsistency in formal specifications, and inconsistency in nonclassical logics and argumentation systems. The deadline for submitting papers is March 8, 2001. For further information, see the Web site.

    TPHOLs 2001

    The fourteenth international conference on Theorem Proving in Higher Order Logics will be held September 3-6, 2001, in Edinburgh, Scotland. The program committee welcomes submissions on all aspects of theorem proving in higher-order logics and on related topics in theorem proving and verification. Of interest are papers in hardware and software verification, refinement, and synthesis; verification of security and communications protocols; formal specification and requirements analysis of systems; industrial applications of theorem provers; advances in theorem prover technology; comparisons of various approaches to theorem proving; proof automation and decision procedures; incorporation of theorem provers into larger systems; combination of theorem provers with other provers and tools; user interfaces for theorem provers; and development and extension of higher-order logics.

    Two categories of submission are invited:

    A: Full research papers. These will be fully refereed, and accepted papers will be published as a volume of Springer-Verlag's Lecture Notes in Computer Science series.

    B: Informal progress reports. These will not be formally refereed, but their content and relevance will be reviewed. Those submissions accepted will be published in a technical report.

    Papers should be no more than 16 pages and written using LaTeX2e and the LNCS style file. Submission deadlines: February 23, 2001 (Category A), and May 18, 2001 (Category B).

    For more information see the Web page.

    CHARME 2001

    CHARME 2001 is the eleventh in a series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the design and verification of hardware and systems. This year CHARME will take place September 4-7, 2001, in Livingston-Edinburgh, Scotland, and will include a full day of tutorials aimed at industrial participation and joint sessions with TPHOLs 2001.

    The conference will cover original research results, case studies, use of technologies across application domains, and reports on practical experiments. Papers (max. 15 pages) describing original work in all aspects of formal hardware and system design and verification methods are invited. The deadline for submission is February 23, 2001. For information, see the Web site.

    The conference proceedings will appear as a volume in Springer-Verlag's Lecture Notes in Computer Science series and will be available at the conference. Selected contributions may be invited for publication in STTT (International Journal on Software Tools for Technology Transfer, Springer-Verlag).


    An international conference on Logic Programming and Nonmonotonic Reasoning will be held in Vienna, Austria, September 17-19, 2001. The conference seeks to facilitate interactions between researchers interested in the design and implementation of logic-based programming languages and database systems, and researchers who work in the areas of knowledge representation and non-monotonic reasoning. LPNMR strives to encompass these theoretical and experimental studies that lead to the construction of practical systems for declarative programming and knowledge representation. Papers (max. 13 pages, Springer LNCS style) should be submitted by April 3, 2001. For details, see the Web site.


    A joint German/Austrian conference on artificial intelligence will take place in Vienna, Austria, September 19-21, 2001. Research and application papers in artificial intelligence are solicited; automated reasoning and knowledge representation are among the possible topics. Papers (max. 15 pages, Springer LNCS style) should be submitted by April 9, 2001. For details, see the Web site.

    ASCM 2001

    The fifth Asian Symposium on Computer Mathematics will take place September 26-28, 2001, at Matsuyama, Japan. ASCM 2001 will provide an international forum for researchers to review the current state of the art and trends, to report research results and progress, and to exchange ideas for future developments in computer mathematics. Topics of interest to AAR readers include automated mathematical reasoning and computer-aided problem solving and instruction.

    Potential participants are invited to submit their papers (max. 10 pages) by March 31, 2001. Accepted papers will be published in the proceedings, which will be distributed to the participants at the conference. For further information, see the Web site.

    New Book on Automated Reasoning with Otter

    A new book entitled Automated Reasoning with Otter, by John Arnold Kalman (with a foreword by Larry Wos), presents an intriguing and thorough treatment of automated reasoning and Otter. The early chapters lead the reader through Otter's fundamental operations and show how to present questions and problems to Otter, beginning with simple examples and including numerous exercises that proceed gently from the basic to the complex. Chapters 6-9 provide a fuller treatment of such concepts as substitution and hyperresolution; the fine detail is complemented nicely by illustrations and case studies, as well as cryptarithmetic puzzles. Chapter 10 shows how, with the help of more sophisticated techniques, the class of reasoning problems that Otter can attack can be greatly extended. In particular, this chapter focuses on propositional connectives such as "not", "or", and "and", and discusses the notion of "logical equivalence." The remaining chapters, Chapters 11-15, are concerned mainly with logical problems whose solution requires reasoning about equality.

    Readership: College students, teachers, and researchers
    551 pages, with CD-ROM
    Hard cover, 10x7 inches
    February 2001
    ISBN 1-58949-004-5
    Rinton Press

    Gail Pieper 2001-01-29