ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 48, August 2000

Contents

From the AAR President
Proofs within Proofs
Boolean Algebra and the Sheffer Stroke Problem
Abstracts of Recent Ph.D. Theses in AR
Journal News

  • Journal of Automated Reasoning
  • Journal of Symbolic Computation - Rings
  • Journal of Symbolic Computation - First-Order Theorem Proving

  • McCune Receives Herbrand Award
    News from CADE Inc.
    White Papers Invited
    Conference Announcements
  • FLoC'02
  • LICS
  • ACL2 Workshop 2000
  • IJCAR
  • RTA
  • From the AAR President, Larry Wos...

    Thanks to Maria Paola Bonacina's encouragement, we are beginning to hear from new Ph.D. graduates in automated reasoning. In this issue we include abstracts of three recent doctoral theses. I hope to hear more from these researchers soon.

    In this regard, I am delighted to include an article by a Ph.D. student, Branden Fitelson, on finding "proofs within proofs" and then--so dear to my heart--"elegantizing" the proofs. In his article, Fitelson mentions the so-called Sheffer stroke, for which a number of simplifications have been published. Also in this issue of the AAR Newsletter, Robert Veroff reports on his current research on the Sheffer stroke, work that he is doing in collaboration with several colleagues including Fitelson.

    Finally, I am pleased to announce that Bill McCune has won the Herbrand Award for the year 2000. He is indeed a fine researcher and a superb colleague.

    Proofs within Proofs


    Branden Fitelson
    University of Wisconsin-Madison (fitelson@students.wisc.edu)

    1. Introduction



    If one surveys the logical literature, one will find more than a few examples of proofs that are less than fully rigorous from an axiomatic point of view. In particular, one will find many proofs in which detachment plus substitution (DS) is used instead of pure condensed detachment (CD). While it is known that any theorem provable with DS is provable with CD (and vice versa
    1), it is not always easy to turn a DS proof into a CD proof. Sometimes we get lucky and a known DS proof is already a CD proof. But, usually, DS proofs contain gaps. Filling these gaps in DS proofs often requires several CD steps. As such, it is useful to think of DS proofs as incomplete "proof sketches'' that must be completed. When a DS proof sketch is turned into a complete CD proof, the resulting CD proof will contain the DS proof sketch as a "proof within a proof''.

    In the present note, I look at a famous historical example of DS proofs that is nontrivial to convert into a CD proof. I also discuss how OTTER can be used to perform the translation and to help one find the shortest CD proof containing all the formulas in a known DS proof.

    2. An Example: A \Lukasiewicz Single Axiom



    \Lukasiewicz [3, pages 299-300] reports a 28-step DS proof sketch of the three Tarski-Bernays axioms for classical, two-valued implication from his (shortest) implicational single axiom. Some of the steps of \Lukasiewicz's DS proof sketch are correct from a CD point of view. But, several of the steps require less than most general instantiations (i.e., unifications). So, these steps are really gaps, from a CD point of view.

    What we want is a CD proof containing all of the 28 steps of \Lukasiewicz's DS proof sketch. In fact, we'd like to find the shortest such proof. This is where OTTER comes in. We can very efficiently search for the desired proof by using the following three OTTER tricks:

    1. First, we place the disjunction of the denials of each of the 28 steps in \Lukasiewicz's DS proof sketch in the usable list. This tells OTTER to stop only when it has found a proof that contains all of the 28 steps in \Lukasiewicz's DS proof sketch (i.e., a refutation of all 28 denials).2

    2. To help guide OTTER's search, we also place all of the (positive) 28 steps of \Lukasiewicz's DS proof sketch either in the hints list or in a weight_list (or both), to be given a low weight either as hints [4] or as resonators [10] (or both). This tells OTTER to key on \Lukasiewicz's steps during the search, thereby leading OTTER to the desired proof as quickly as possible. I have found that, when trying to fill gaps in DS proofs, using both resonators and hints is most effective.

    3. Finally, we place \Lukasiewicz's single axiom (plus CD) in the hot list. The hot list strategy [11] is very effective in single axiom problems for filling gaps (and for finding proofs in general). I have found that setting the heat parameter even as high as 8 or more can greatly speed OTTER's finding of proofs from single axioms (see also [8]).

    In the APPENDIX is an OTTER input file that implements this basic proof-finding strategy. Using this basic input file, OTTER finds a proof in just a few minutes. The first proof it finds contains 47 CD steps.

    Once a proof is found, the process of elegantization begins. Larry Wos and I have developed many strategies for aiding the search for elegant proofs in formal logic [7, 6, 9, 1]. Using these strategies, we have been able to find a 36-step CD proof that contains all 28 of \Lukasiewicz's DS proof sketch steps (included in the APPENDIX). This is the shortest such proof we have been able to find.

    I leave it as a challenge problem for AAR newsletter readers to try to improve on our 36-step CD completion of \Lukasiewicz's 28-step DS proof sketch.

    Some Other Historical Examples

    Mordchaj Wajsberg was a student of \Lukasiewicz. In his master's thesis, Wajsberg reports several DS proofs that contain many large gaps, from a CD point of view. In particular, [5, pages 192-195] reports DS proofs of three axiomatizations for the implicational fragment of classical two-valued sentential logic. Each of these proofs contains several rather large gaps, from a CD point of view. Wajsberg also reports DS proof sketches for four axiomatizations of the equivalential calculus [5, pages 195-198], as well as an axiomatization of two-valued logic, based on Sheffer's stroke [5, pages 37-38].

    Appendix

    Basic OTTER Input File for \Lukasiewicz Problem

    set(hyper_res).
    assign(max_weight, 32).
    assign(max_distinct_vars, 8).
    assign(heat,2).
    clear(print_kept).  
    clear(print_new_demod).
    clear(print_back_demod).
    clear(print_back_sub).
    set(order_history).
    set(input_sos_first).
    assign(bsub_hint_wt, 1).
    set(keep_hint_subsumers).
    
    list(hints).
    % Following is Lukasiewicz's 28 step DS proof sketch (as hints)
    P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(x,i(y,u)))).
    P(i(i(i(x,i(y,z)),i(i(x,y),i(u,y))),i(v,i(i(x,y),i(u,y))))).
    P(i(i(i(x,y),x),i(z,x))).
    P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))).
    P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))).
    P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))).
    P(i(i(i(x,y),z),i(y,z))).
    P(i(x,i(i(x,y),i(z,y)))).
    P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))).
    P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))).
    P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))).
    P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))).
    P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))).
    P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))).
    P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))).
    P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))).
    P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))).
    P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,z),u),i(x,y)))).
    P(i(i(i(i(x,y),y),i(z,y)),i(i(i(y,u),x),i(z,y)))).
    P(i(i(i(i(x,y),z),z),i(i(z,y),i(x,y)))).
    P(i(x,x)).
    P(i(i(i(x,y),z),i(i(z,x),x))).
    P(i(x,i(i(x,y),y))).
    P(i(i(x,y),i(i(i(x,z),y),y))).
    P(i(i(i(i(x,y),i(i(y,z),i(x,z))),i(i(i(x,z),y),y)),i(i(i(x,z),y),y))).
    P(i(x,i(y,x))).
    P(i(i(i(x,y),x),x)).
    P(i(i(x,y),i(i(y,z),i(x,z)))).
    end_of_list.
    
    weight_list(pick_and_purge).
    % Following is Lukasiewicz's 28 step DS proof sketch (as resonators)
    weight(P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(x,i(y,u)))),2).
    weight(P(i(i(i(x,i(y,z)),i(i(x,y),i(u,y))),i(v,i(i(x,y),i(u,y))))),2).
    weight(P(i(i(i(x,y),x),i(z,x))),2).
    weight(P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))),2).
    weight(P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))),2).
    weight(P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))),2).
    weight(P(i(i(i(x,y),z),i(y,z))),2).
    weight(P(i(x,i(i(x,y),i(z,y)))),2).
    weight(P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))),2).
    weight(P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))),2).
    weight(P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))),2).
    weight(P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))),2).
    weight(P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))),2).
    weight(P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))),2).
    weight(P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))),2).
    weight(P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))),2).
    weight(P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))),2).
    weight(P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,z),u),i(x,y)))),2).
    weight(P(i(i(i(i(x,y),y),i(z,y)),i(i(i(y,u),x),i(z,y)))),2).
    weight(P(i(i(i(i(x,y),z),z),i(i(z,y),i(x,y)))),2).
    weight(P(i(x,x)),2).
    weight(P(i(i(i(x,y),z),i(i(z,x),x))),2).
    weight(P(i(x,i(i(x,y),y))),2).
    weight(P(i(i(x,y),i(i(i(x,z),y),y))),2).
    weight(P(i(i(i(i(x,y),i(i(y,z),i(x,z))),i(i(i(x,z),y),y)),i(i(i(x,z),y),y))),2).
    weight(P(i(x,i(y,x))),2).
    weight(P(i(i(i(x,y),x),x)),2).
    weight(P(i(i(x,y),i(i(y,z),i(x,z)))),2).
    end_of_list.
    
    list(usable).
    % Following is condensed detachment (CD)
    -P(i(x,y)) | -P(x) | P(y).
    
    % Following is disjunction of denials of 28 DS proof sketch steps
    -P(i(i(i(i(c3,c1),i(c4,c1)),i(c1,c2)),i(c3,i(c1,c2)))) | 
    -P(i(i(i(c3,i(c1,c2)),i(i(c3,c1),i(c4,c1))),i(c5,i(i(c3,c1),i(c4,c1))))) | 
    -P(i(i(i(c1,c2),c1),i(c4,c1))) | 
    -P(i(i(i(c4,c1),i(c1,c2)),i(c3,i(c1,c2)))) | 
    -P(i(i(i(c3,i(c1,c2)),i(c4,c1)),i(c5,i(c4,c1)))) |
    -P(i(i(i(c5,i(c4,c1)),i(c3,i(c1,c2))),i(c6,i(c3,i(c1,c2))))) | 
    -P(i(i(i(c4,c2),c1),i(c2,c1))) | 
    -P(i(c3,i(i(c3,c1),i(c4,c1)))) | 
    -P(i(i(i(i(i(c3,c2),c1),i(c4,c1)),c3),i(c5,c3))) | 
    -P(i(i(i(c5,c3),i(i(i(c3,c2),c1),i(c4,c1))),i(c6,i(i(i(c3,c2),c1),i(c4,c1))))) | 
    -P(i(i(i(c6,i(i(i(c3,c2),c1),i(c4,c1))),i(c5,c3)),i(c7,i(c5,c3)))) | 
    -P(i(i(i(c7,i(c5,c3)),i(c6,i(i(i(c3,c2),c1),i(c4,c1)))),i(c8,i(c6,i(i(i(c3,c2),c1),i(c4,c1)))))) |
    -P(i(i(i(c5,c3),i(c4,c1)),i(i(i(c3,c2),c1),i(c4,c1)))) | 
    -P(i(i(i(c3,c2),i(c4,c1)),i(i(c3,c1),i(c4,c1)))) | 
    -P(i(i(c3,i(c4,c1)),i(i(i(c3,c2),c1),i(c4,c1)))) |
    -P(i(i(i(i(i(c1,c2),c3),c5),i(c4,c1)),i(i(c3,c1),i(c4,c1)))) |
    -P(i(i(i(i(c3,c1),i(c4,c1)),i(i(i(c1,c2),c3),c5)),i(c6,i(i(i(c1,c2),c3),c5)))) |
    -P(i(i(i(i(c4,c1),c2),i(c3,c1)),i(i(i(c1,c2),c3),i(c4,c1)))) |
    -P(i(i(i(i(c3,c1),c1),i(c4,c1)),i(i(i(c1,c2),c3),i(c4,c1)))) | 
    -P(i(i(i(i(c1,c3),c2),c2),i(i(c2,c3),i(c1,c3)))) | 
    -P(i(c1,c1)) | 
    -P(i(i(i(c1,c2),c3),i(i(c3,c1),c1))) | 
    -P(i(c3,i(i(c3,c1),c1))) | 
    -P(i(i(c1,c2),i(i(i(c1,c3),c2),c2))) | 
    -P(i(i(i(i(c1,c2),i(i(c2,c3),i(c1,c3))),i(i(i(c1,c3),c2),c2)),i(i(i(c1,c3),c2),c2))) | 
    -P(i(c1,i(c2,c1))) | 
    -P(i(i(i(c1,c2),c1),c1)) | 
    -P(i(i(c1,c2),i(i(c2,c3),i(c1,c3)))) | $ANS(28_luka_steps).
    end_of_list.
    
    list(sos).
    % Following is Lukasiewicz's shortest implicational single axiom
    P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
    end_of_list.
    
    list(hot).
    % Following is condensed detachment (CD)
    -P(i(x,y)) | -P(x) | P(y).
    
    % Following is Lukasiewicz's shortest implicational single axiom
    P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
    end_of_list.
    

    36-Step CD Proof Containing \Lukasiewicz's DS Proof Sketch

    Length of proof is 36.  Level of proof is 29.
    
    ---------------- PROOF ----------------
    
    34 [] -P(i(x,y))| -P(x)|P(y).
    35 [] -P(i(i(i(i(c3,c1),i(c4,c1)),i(c1,c2)),i(c3,i(c1,c2)))) | ...
    36 [] P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
    39 [hyper,34,36,36] P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(v,i(y,u)))).
    41 [hyper,34,36,39] P(i(i(i(x,i(y,z)),i(i(u,y),i(v,y))),i(w,i(i(u,y),i(v,y))))).
    46 [hyper,34,41,36] P(i(x,i(i(i(y,z),y),i(u,y)))).
    47 [hyper,34,46,46] P(i(i(i(x,y),x),i(z,x))).
    51 [hyper,34,36,47] P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))).
    52 [hyper,34,36,51] P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))).
    54 [hyper,34,36,52] P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))).
    57 [hyper,34,54,36] P(i(x,i(i(i(y,z),u),i(z,u)))).
    58 [hyper,34,57,57] P(i(i(i(x,y),z),i(y,z))).
    60 [hyper,34,58,58] P(i(x,i(y,x))).
    62 [hyper,34,58,36] P(i(x,i(i(x,y),i(z,y)))).
    81 [hyper,34,36,62] P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))).
    93 [hyper,34,36,81] P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))).
    98 [hyper,34,36,93] P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))).
    101 [hyper,34,36,98] P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))).
    106 [hyper,34,101,36] P(i(x,i(i(i(y,z),i(u,v)),i(i(i(z,w),v),i(u,v))))).
    107 [hyper,34,106,106] P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))).
    113 [hyper,34,107,36] P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))).
    117 [hyper,34,113,62] P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))).
    132 [hyper,34,117,36] P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))).
    136 [hyper,34,36,132] P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))).
    140 [hyper,34,132,58] P(i(i(x,y),i(x,y))).
    143 [hyper,34,136,136] P(i(x,i(i(i(i(y,z),u),i(v,z)),i(i(i(z,w),v),i(y,z))))).
    153 [hyper,34,143,143] P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,v),u),i(x,y)))).
    158 [hyper,34,107,153] P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,v),x),i(u,y)))).
    172 [hyper,34,158,140] P(i(i(i(x,y),z),i(i(z,x),x))).
    175 [hyper,34,158,113] P(i(i(i(i(x,y),z),u),i(i(u,y),i(x,y)))).
    185 [hyper,34,58,172] P(i(x,i(i(x,y),y))).
    191 [hyper,34,172,140] P(i(i(i(x,y),x),x)).
    225 [hyper,34,175,52] P(i(i(i(x,i(y,z)),i(z,u)),i(v,i(z,u)))).
    234 [hyper,34,113,185] P(i(i(x,y),i(i(i(x,z),y),y))).
    270 [hyper,34,58,191] P(i(x,x)).
    276 [hyper,34,36,225] P(i(i(i(x,i(y,z)),i(u,i(v,y))),i(w,i(u,i(v,y))))).
    278 [hyper,34,234,234] P(i(i(i(i(x,y),z),i(i(i(x,u),y),y)),i(i(i(x,u),y),y))).
    317 [hyper,34,175,278] P(i(i(i(i(i(x,y),z),z),u),i(i(x,z),u))).
    337 [hyper,34,317,175] P(i(i(x,y),i(i(y,z),i(x,z)))).
    346 [hyper,35,225,...] $ANS(28_luka_steps).
    
    ------------ end of proof -------------
    



    References



    [1] B. Fitelson and L. Wos. Finding missing proofs with automated reasoning. Studia Logica (to appear).

    [2] J. Kalman. Condensed detachment as a rule of inference. Studia Logica, 42:443-451, 1983.

    [3] J. \Lukasiewicz. Selected Works. Noth Holland, 1970.

    [4] R. Veroff. Using hints to increase the effectiveness of an automated reasoning program: Case studies. Journal of Automated Reasoning, 16(3):223-239, 1996.

    [5] M. Wajsberg. Logical Works. Polish Academy of Sciences, Wroc\law, 1977.

    [6] L. Wos. Automating the search for elegant proofs. Journal of Automated Reasoning, 21(2):135-175, 1998.

    [7] L. Wos. The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial. Academic Press, 1996.

    [8] L. Wos. Conquering the Meredith single axiom. Preprint ANL/MCS/P815-0500. Mathematics and Computer Science Division, Argonne National Laboratory.

    [9] L. Wos. A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, 1999.

    [10] L. Wos. The resonance strategy. Computers and Mathematics with Applications, 29(2):133-178, 1995.

    [11] L. Wos with G. W. Pieper. The hot list strategy. Journal of Automated Reasoning, 22(1):1-44, 1999.

    Boolean Algebra and the Sheffer Stroke Problem


    Robert Veroff (veroff@cs.unm.edu)
    University of New Mexico

    My colleagues and I are using Otter to find short bases for Boolean algebra in terms of the Sheffer stroke. An ongoing report of this work is available on the Web page.

    Abstracts of Recent Ph.D. Theses in AR

    In the last issue of the AAR newsletter, we initiated a new section featuring abstracts of recent doctoral dissertations in automated deduction and theorem proving. This time we have three abstracts to include.

    1. Title: Superposition Theorem Proving for Commutative Algebraic Theories

    Author: Jürgen Stuber

    Advisor: Harald Ganzinger

    Defense date: June 2000

    Institution: Max-Planck-Institute for Computer Science, Saarbrücken, Germany

    Abstract: We develop special superposition calculi for first-order theorem proving in the theories of Abelian groups, commutative rings, and modules and commutative algebras over fields or over the ring of integers, in order to make automated theorem proving in these theories more effective. The calculi are refutationally complete on arbitrary sets of ground clauses, which in particular may contain additional function symbols. The ground calculi are derived systematically from a representation of the theory as a convergent term rewriting system. Compared wuth standard superposition, they have stronger ordering restrictions so that inferences are applied only to maximal summands, and they contain macro inference rules that use theory axioms in a goal directed fashion. In general we need additional inferences to handle critical peaks between extended clauses. We show that these are not needed for Abelian groups and modules, and that for commutative rings and commutative algebras one such inference suffices for any pair of ground clauses. To facilitate the construction of term orderings for such calculi, we introduce theory path orderings.

    2. Title: Reasoning about Terminating Functional Programs

    Advisor: Tobias Nipkow

    Author: Konrad Slind

    Institution: Institut für Informatik, Technische Universität München

    Defense date: November 15, 1999

    Abstract: This thesis addresses two basic problems with the current crop of mechanized proof systems. The first problem is largely technical: the act of soundly introducing a recursive definition is not as simple and direct as it should be. The second problem is largely social: there is very little code-sharing between theorem prover implementations; as a result, common facilities are typically built anew in each proof system, and the overall progress of the field is thereby hampered.

    We use the application domain of functional programming to explore the first problem. We build a pattern-matching style recursive function definition facility, based on mechanically proven well-founded recursion and induction theorems. Reasoning support is embodied by automatically derived induction theorems, which are customized to the recursion structure of definitions. This provides a powerful, guaranteed sound, definition-and-reasoning facility for functions that strongly resemble programs in languages such as ML or Haskell. We demonstrate this package (called TFL) on several well-known challenge problems.

    In spite of its power, the approach suffers from a low level of automation, because a termination relation must be supplied at function definition time. If humans are to be largely relieved of the task of proving termination, it must be possible for the act of defining a recursive function to be completely separate from the act of finding a termination relation for it and proving the ensuing termination conditions. We show how this separation can be achieved, while still preserving soundness. Building on this, we present a new way to define program schemes and prove high-level program transformations.

    Since the second problem is largely social, we cannot solve it alone; however, we do present an artifact that marks a path to a brighter future. In particular, we show that the sophisticated algorithms implemented in TFL can be parameterized by a higher order logic proof system. The package has been instantiated to HOL and Isabelle-HOL, two quite different mechanizations of higher order logic. In this exercise, we found that the fully formal approach taken to justifying definitions and deriving induction schemes was fundamental in providing the required combination of portability and soundness.

    Current Address: University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom. E-mail Address: kxs@cl.cam.ac.uk

    3. Title: Soft Typing for Clausal Inference Systems

    Author: Christoph Meyer

    Advisor: Prof. H. Ganzinger, MPI, Saarbrücken

    Institution: University of Saarbrücken, Germany, 1999

    Abstract: The purpose of this thesis is to study methods for the semantical control of automated theorem proving systems for first-order logic (with equality) based on certain effective abstraction techniques. We propose a general framework called soft typing for clausal inference systems to incorporate the validity/satisfiability of clauses with respect to certain model hypotheses into the control of inference systems. The effectiveness of the method is obtained by inferring automatically abstractions that result in approximations of validity/satisfiability of clauses with respect to these models. For an effective use of soft typing for ordered resolution and superposition, we propose the use of sets of Horn clauses (with equality) to represent approximations of model hypotheses for sets of clauses. We show that certain decidable fragments of first-order logic without equality can be generalized to non-trivial decidable (equational) fragments. The satisfiability of clauses with respect to the approximations implies the satisfiability in the original model hypotheses.

    See the Web site for the full version.

    Journal News

    Searchable Index for the Journal of Automated Reasoning

    The Journal of Automated Reasoning now has online an index of all the articles since its founding in 1985. Included are keywords, which researchers may find useful in locating an article relevant to their studies. The information is available from the JAR Web page.

    We remind readers that the Journal is available to AAR members at a dramatically reduced price: $79 instead of the regular $242.

    Special Issue of JSC on Rings

    The deadline for submission to the special issue of the Journal of Symbolic Computation on "Effective Methods in Rings of Differential Operators" has been extended to October 15, 2000.

    For more details see the Web page.

    Special Issue of JSC on First-Order Theorem Proving

    A special issue of the Journal of Symbolic Computation will be edited to commemorate the recent success of FTP 2000, the third workshop on First-Order Theorem Proving. Like FTP 2000 itself, the special issue will focus on first-order theorem proving as a core theme of automated deduction. The editors of this special issue, Peter Baumgartner and Hantao Zhang, welcome original, unpublished contributions; contributions are not limited to those presented at FTP 2000. Submissions should be sent by e-mail in Postscript format to ftp00@cs.uiowa.edu, accompanied by a plain text abstract. The deadline is October 1, 2000.

    McCune Receives Herbrand Award

    William McCune has been named recipient of the Herbrand Award for the year 2000. The award is given by Conference on Automated Deduction (CADE) Inc. to honor exceptional contributions to the field of automated deduction.

    McCune is a senior scientist in the Mathematics and Computer Science Division at Argonne National Laboratory. He was cited for his outstanding success in answering the Robbins question, which had challenged mathematicians and logicians for six decades, and for his design of the powerful program OTTER, which has become a benchmark for automated deduction programs. McCune's contributions to the field also include powerful inference rules and numerous new strategies that have dramatically increased the likelihood of finding a proof. Indeed, McCune has answered numerous open questions in such diverse areas as combinatory logic, group theory, algebra, and logic calculi.

    The Herbrand Award was presented at the CADE-17 in June 2000 in Pittsburgh.

    News from CADE Inc.
    Maria Paola Bonacina
    (Secretary of AAR and CADE)
    e-mail: bonacina@cs.uiowa.edu

    1. Amendment to the CADE Inc. Bylaws

    The following amendment to the CADE Inc. bylaws was proposed by David Plaisted, and approved at the Business Meeting of CADE-17 with strong support. A ballot to vote on this amendment was distributed to the membership on July 6 with time to vote until August 31, 2000.

    Proposed Amendment to the CADE Bylaws, by David A. Plaisted

    The following amendment to the bylaws of CADE passed with an overwhelming majority at the CADE 2000 business meeting, and is now being put to a vote of the entire membership of the AAR:

    The number of trustees elected following each CADE conference will be increased from two to three, while maintaining their term at three CADE conferences, normally three years. This means that there will be a total of nine elected trustees instead of six. The number of elected trustees is currently six, and will increase by one at each trustee election following CADE 2000 until the total reaches nine. For an amendment to pass, at least 30\% of the AAR membership must vote on it, and of those voting, at least two thirds must vote in favor. Therefore every vote matters, and your vote is very important.

    Justification of the Proposed Amendment, by David A. Plaisted

    In every trustee election so far, there have been more than two qualified candidates, and there is no reason why a third candidate cannot serve as a trustee. CADE is facing some challenges and opportunities now. Three more bright and qualified trustees would be a significant help in meeting these. This amendment would make it easier to elect trustees from areas such as AI and hardware verification, and thereby broaden the scope and appeal of CADE. Currently there are three ex officio trustees who are appointed but not elected, namely, the secretary, the treasurer, and the upcoming program chair. There are also six elected trustees. This amendment would make CADE more democratic, since roughly 3/4 of the trustees would be elected instead of 2/3 as at present. This would give you, the members of the AAR, a greater voice in CADE.

    2. Upcoming CADE Trustee Elections

    The following people are currently serving as Trustees of CADE Inc.:

    Ulrich Furbach, President (Elected 8/1997)
    Frank Pfenning, Vice-President (Elected 10/1998)
    Harald Ganzinger (Past Program Chair, elected 10/1999)
    Claude Kirchner (Past Program Co-chair, elected 10/1998)
    William W. McCune (Past Program Chair, elected 8/1997)
    David A. Plaisted (Elected 10/1999)
    Maria Paola Bonacina (Secretary)
    Neil V. Murray (Treasurer)
    Tobias Nipkow (IJCAR 2001 Program Co-Chair)

    The terms of Ulrich Furbach and William McCune are expiring, leaving two positions to be filled. If the above amendment is approved, it will be implemented by introducing a new position for three consecutive elections. For instance, at the next election, there will be three, rather than two, open positions. The following candidates were nominated for the next CADE Trustee elections:

    Ulrich Furbach
    Michael Kohlhase
    David McAllester
    Andrei Voronkov
    Dongming Wang

    All AAR members will receive a ballot for this election.

    White Papers Invited

    The Office of Naval Research invites researchers to submit white papers and proposals on the topic of Digital Libraries for Constructive Mathematical Knowledge. The objective is to create a digital library of algorithms and constructive mathematics usable for program and software construction. Among the research concentration areas listed is proof-checking and model checking for certifying proofs of the standard body of computationally related mathematics. White papers (6 pages or less) are due August 17, 2000.

    For further information, see the Web page.

    Conference Announcements

    FLoC'02

    The third Federated Logic Conference (FLoC'02) will be held in Copenhagen, Denmark, July 20 - August 1, 2002. Pre-conference workshops will be held on July 20-21. Three conferences will be held in parallel during July 22-25:

    1. Formal Methods (FM)
    2. IEEE Symposium on Logic in Computer Science (LICS - see article below)
    3. Conference on Rewriting Techniques and Applications (RTA)
    Mid-conference workshops and excursions will be on July 25-26. Two conferences are scheduled in parallel for July 27-30:
    1. Conference on Automated Deduction (CADE)
    2. Conference on Computer-Aided Verification (CAV)
    Post-conference workshops will be held on July 31 - August 1. Plenary events involving all the conferences are planned.

    Calls for papers and call for workshop proposals will be issued in the near future. For additional information regarding the participating meetings, please check the FLoC Web page later this fall.

    LICS

    The sixteenth annual IEEE Symposium on Logic in Computer Science will be held on June 16-19, 2001, in Boston, Massachusetts. LICS is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense.

    Suggested topics of interest for paper submissions include abstract data types, automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, logic in databases, domain theory, finite model theory, formal aspects of program analysis, formal methods, hybrid systems, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logics of programs, logic programming, modal and temporal logics, model checking, programming language semantics, reasoning about security, rewriting, specifications, type systems and type theory, and verification. The deadline for submissions is January 8, 2001.

    LICS 2001 also will have a session of short (5-10 minute) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages) will be due March 31, 2001.

    Researchers and practitioners also are invited to submit proposals for workshops. Proposals should consist of two parts. First, a short scientific justification of the proposed topic, its significance, and the particular benefits of a workshop. A second, organizational, part should include contact information for organizers; proposed format and agenda; procedures for selecting papers and participants; and duration and preferred period (pre- or post-LICS). Proposals are due October 1, 2000, and should be sent to Leonid Libkin, e-mail: libkin@research.bell-labs.com.

    For further information, see the LICS Web site for details.

    ACL2 Workshop 2000

    The next workshop on the ACL2 theorem prover and its applications will be held at the University of Texas on Monday and Tuesday, October 30-31, 2000. Immediately after the ACL2 workshop, Austin will host the Formal Methods in Computer-Aided Design (FMCAD) conference. It will be easy to attend both.

    This year's ACL2 workshop is open to all. For those who don't know ACL2 but wish to learn enough to listen to the talks and see what's going on in the ACL2 community, we will present a brief tutorial on Sunday afternoon, October 29, before the meeting.

    There will be a nominal registration fee to cover the cost of food, the meeting room, and (we expect) the proceedings, to be produced and mailed after the meeting. We anticipate the fee being around $100 and will give full details when the details have been finalized. The fee will be collected by check or cash at the workshop.

    For details, see the Web site.

    IJCAR

    The International Joint Conference on Automated Reasoning (IJCAR) is the fusion of three major conferences in Automated Reasoning: CADE (International Conference on Automated Deduction), TABLEAUX (international conference on automated reasoning with analytic tableaux and related methods), and FTP (international workshop on First-Order Theorem Proving). These three events will join for the first time at the IJCAR conference in Siena in June 2001.

    Research papers. IJCAR 2001 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers (up to 15 pages) and descriptions of working automated deduction systems (up to 5 pages) are solicited. All submissions must be received by January 14, 2001.

    Note: A prize of 500 Euros will be given to the best paper, as judged by the program committee, written solely by one or more full-time students.

    Short papers (up to 10 pages) are also solicited. These are intended for quick dissemination of work in progress or results not substantial enough for a full research paper. Authors of accepted papers are expected to present a brief outline of their work at the conference and to prepare a poster for display at the conference venue. The submission deadline is April 2, 2001.

    Tutorials. Proposals (1-2 pages) for tutorials are also solicited. At present, the tutorials are scheduled to take place on June 18-19. The deadline for submission of is January 15, 2001.

    Workshops. Researchers and practitioners are invited to submit proposals (2 pages) for workshops on IJCAR-related topics. Workshops that close the gap between automated reasoning and related areas -- for instance, formal methods or software engineering -- are especially encouraged. The deadline for submission is January 1, 2001.

    For details, see the Web site.

    RTA

    The 12th International Conference on Rewriting Techniques and Applications will take place on May 22-24, 2001, at the Sea of Galilee, Israel.

    Papers are solicited on all aspects of rewriting, including applications, foundations, frameworks, implementation, and semantics. Submissions should fall into one of the following categories: (1) regular research papers describing new results, judged on correctness and significance (15 pages); (2) papers describing the experience of applying rewriting techniques in other areas, judged on relevance and comparison with other approaches (15 pages); (3) problem sets that provide realistic and interesting challenges in the field of rewriting (15 pages); and (4) system descriptions, containing a link to a working system to be judged on usefulness and design (4 pages).

    Note: A prize of 2001 NIS will be given to the best paper as judged by the program committee.

    For details about the conference and submissions, see the Web site.