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
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.
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 ukasiewicz Single Axiom
ukasiewicz [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
ukasiewicz'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 ukasiewicz'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:
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 ukasiewicz'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 ukasiewicz's 28-step DS proof sketch.
Some Other Historical Examples
Mordchaj Wajsberg was a student of ukasiewicz. 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 ukasiewicz 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 ukasiewicz'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. ukasiewicz. 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, Wrocaw, 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.
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.
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.
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.
For more details see the Web page.
Special Issue of JSC on First-Order Theorem Proving
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.
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.
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.
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.
For further information, see the LICS Web site for details.
For details, see the Web site.
For details, see the Web site.
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.