%!PS-Adobe-2.0
%%Title: cade90.mss
%%DocumentFonts: (atend)
%%Creator: Dianne King and Scribe 7(1700)
%%CreationDate: 16 April 1990 16:24
%%Pages: (atend)
%%EndComments
% PostScript Prelude for Scribe.
/BS {/SV save def 0.0 792.0 translate .01 -.01 scale} bind def
/ES {showpage SV restore} bind def
/SC {setrgbcolor} bind def
/FMTX matrix def
/RDF {WFT SLT 0.0 eq
{SSZ 0.0 0.0 SSZ neg 0.0 0.0 FMTX astore}
{SSZ 0.0 SLT neg sin SLT cos div SSZ mul SSZ neg 0.0 0.0 FMTX astore}
ifelse makefont setfont} bind def
/SLT 0.0 def
/SI { /SLT exch cvr def RDF} bind def
/WFT /Courier findfont def
/SF { /WFT exch findfont def RDF} bind def
/SSZ 1000.0 def
/SS { /SSZ exch 100.0 mul def RDF} bind def
/AF { /WFT exch findfont def /SSZ exch 100.0 mul def RDF} bind def
/MT /moveto load def
/XM {currentpoint exch pop moveto} bind def
/UL {gsave newpath moveto dup 2.0 div 0.0 exch rmoveto
setlinewidth 0.0 rlineto stroke grestore} bind def
/LH {gsave newpath moveto setlinewidth
0.0 rlineto
gsave stroke grestore} bind def
/LV {gsave newpath moveto setlinewidth
0.0 exch rlineto
gsave stroke grestore} bind def
/BX {gsave newpath moveto setlinewidth
exch
dup 0.0 rlineto
exch 0.0 exch neg rlineto
neg 0.0 rlineto
closepath
gsave stroke grestore} bind def
/BX1 {grestore} bind def
/BX2 {setlinewidth 1 setgray stroke grestore} bind def
/PB {/PV save def newpath translate
100.0 -100.0 scale pop /showpage {} def} bind def
/PE {PV restore} bind def
/GB {/PV save def newpath translate rotate
div dup scale 100.0 -100.0 scale /showpage {} def} bind def
/GE {PV restore} bind def
/FB {dict dup /FontMapDict exch def begin} bind def
/FM {cvn exch cvn exch def} bind def
/FE {end /original-findfont /findfont load def /findfont
{dup FontMapDict exch known{FontMapDict exch get} if
original-findfont} def} bind def
/BC {gsave moveto dup 0 exch rlineto exch 0 rlineto neg 0 exch rlineto closepath clip} bind def
/EC /grestore load def
/SH /show load def
/MX {exch show 0.0 rmoveto} bind def
/W {0 32 4 -1 roll widthshow} bind def
/WX {0 32 5 -1 roll widthshow 0.0 rmoveto} bind def
/RC {100.0 -100.0 scale
612.0 0.0 translate
-90.0 rotate
.01 -.01 scale} bind def
/URC {100.0 -100.0 scale
90.0 rotate
-612.0 0.0 translate
.01 -.01 scale} bind def
/RCC {100.0 -100.0 scale
0.0 -792.0 translate 90.0 rotate
.01 -.01 scale} bind def
/URCC {100.0 -100.0 scale
-90.0 rotate 0.0 792.0 translate
.01 -.01 scale} bind def
%%EndProlog
%%Page: 0 1
BS
0 SI
14 /Times-Bold AF
24088 17138 MT
(A Theorem Prover for a)SH
24962 18940 MT
(Computational Logic)SH
10 /Times-Roman AF
34953 22506 MT
(1)SH
12 SS
27186 22887 MT
(Robert S. Boyer)SH
27252 24390 MT
(J Strother Moore)SH
13 SS
25546 29692 MT
(Technical Report 54)SH
27855 31069 MT
(April, 1990)SH
12 SS
25135 52113 MT
(Computational Logic Inc.)SH
24952 53942 MT
(1717 W. 6th St. Suite 290)SH
26336 55771 MT
(Austin, Texas 78703)SH
27570 57600 MT
(\050512\051 322-9951)SH
19440 58832 MT
(This report was)
144 W( the keynote address at the 10th)145 W
19440 60118 MT
(International Conference on Automated)1553 W
19440 61404 MT
(Deduction, July,)
1097 W( 1990 in Kaiserslautern,)1098 W
19440 62690 MT
(W. Germany. The views)
616 W( and conclusions)615 W
19440 63976 MT
(contained in this document are those of)
446 W( the)447 W
19440 65262 MT
(authors and should not be)
771 W( interpreted as)770 W
19440 66548 MT
(representing the official)
1230 W( policies, either)1231 W
19440 67834 MT
(expressed or implied,)
265 W( or Computational Logic,)264 W
10800 50 9504 68885 UL
19440 69120 MT
(Inc. or the U.S. Government.)SH
8 SS
10504 70550 MT
(1)SH
10 SS
10904 70895 MT
(Mailing address: Computer Sciences Department, University of Texas at Austin,)
81 W( Austin, TX 78712,)80 W
9504 72000 MT
(USA)SH
ES
%%Page: 1 2
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(1)SH
15 /Times-Bold AF
28060 8205 MT
(Abstract)SH
12 /Times-Roman AF
9504 12628 MT
(We briefly review a)
96 W( mechanical theorem-prover for a logic of recursive functions over)97 W
9504 13914 MT
(finitely generated objects including)
324 W( the integers, ordered pairs, and symbols. The)323 W
9504 15200 MT
(prover, known both as NQTHM and as the Boyer-Moore prover, contains a mechanized)36 W
9504 16486 MT
(principle of induction and implementations of linear resolution,)
2 W( rewriting, and arithmetic)1 W
9504 17772 MT
(decision procedures. We describe)
50 W( some applications of the prover, including a proof of)51 W
9504 19058 MT
(the correct implementation of a higher level language)
10 W( on a microprocessor defined at the)9 W
9504 20344 MT
(gate level. We also describe)
170 W( the ongoing project of recoding the entire prover as an)171 W
9504 21630 MT
(applicative function within its own logic.)SH
ES
%%Page: 2 3
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(2)SH
14 /Times-Bold AF
9504 8138 MT
(1 Introduction)700 W
12 /Times-Roman AF
9504 10393 MT
(We feel honored to be)
176 W( invited to give the keynote address for CADE-10. We thank)175 W
9504 11679 MT
(Mark Stickel and the program committee for the invitation.)SH
9504 14251 MT
(It has been suggested that we discuss our theorem prover and)
68 W( its application to proving)69 W
9504 15537 MT
(the correctness of computations. We have been working on our prover, on and off,)
2 W( since)1 W
9504 16823 MT
(about 1972)
83 W( [9].)
SH( This)
466 W( prover is known both as the)83 W
/Times-Italic SF
34336 XM
(Boyer-Moore theorem prover)83 W
/Times-Roman SF
49084 XM
(and as)83 W
/Times-Italic SF
9504 18109 MT
(NQTHM.)SH
/Times-Roman SF
14729 XM
(\050pronounced)SH
/Times-Italic SF
21520 XM
(en-que-thum)SH
/Times-Roman SF
(, an acronym for ``New, Quantified THeoreM)425 W
9504 19395 MT
(Prover,'' an uninspired parochialism that)
59 W( has taken on a life of its own\051. The details of)60 W
9504 20681 MT
(our prover and its applications have been extensively presented in several books)
180 W( and)179 W
9504 21967 MT
(articles. In fact, from these publications)
144 W( the prover has been recoded by at least three)145 W
9504 23253 MT
(other groups. In)
387 W( this paper, we will \050a\051 very briefly review the prover and its)386 W
9504 24539 MT
(applications, \050b\051 provide pointers to the literature on the prover and its applications, and)40 W
9504 25825 MT
(\050c\051 discuss ACL2, a new development of the prover which involves recoding)
152 W( it in its)151 W
9504 27111 MT
(own logic, a subset of applicative Common Lisp.)SH
9504 29683 MT
(In the subsequent discussion,)
63 W( we will make reference to two books, which are the main)64 W
9504 30969 MT
(references on NQTHM. They)
320 W( are \050a\051)319 W
/Times-Italic SF
29936 XM
(A Computational Logic)319 W
/Times-Roman SF
42143 XM
([11] which we will)319 W
9504 32255 MT
(abbreviate as ``ACL'' and \050b\051)190 W
/Times-Italic SF
25086 XM
(A Computational Logic Handbook)191 W
/Times-Roman SF
42527 XM
([18] which we will)191 W
9504 33541 MT
(abbreviate as)
134 W( ``ACLH''. Although a decade old, ACL still provides a rather accurate)133 W
9504 34827 MT
(description of many of the prover's)
4 W( heuristics and some simple applications, whereas the)5 W
9504 36113 MT
(much more recent ACLH accurately describes the current logic and user interface.)SH
14 /Times-Bold AF
9504 38483 MT
(2 The)
700 W( Logic)SH
12 /Times-Roman AF
9504 40738 MT
(Although many theorem)
423 W( provers, especially those of the resolution tradition, are)422 W
9504 42024 MT
(designed to work with)
1 W( arbitrary collections of first order axioms, NQTHM is designed to)2 W
9504 43310 MT
(be used mainly)
243 W( with the fixed set of axioms we provide, typically augmented by a)242 W
9504 44596 MT
(number of definitions provided by the NQTHM user. Questions one)
135 W( might ask about)136 W
9504 45882 MT
(the NQTHM theory are)
62 W( ``What are the well-formed formulas, what are the axioms, and)61 W
9504 47168 MT
(what are the rules of inference?'')
48 W( The)
397 W( precise answers to these questions may be found)49 W
9504 48454 MT
(in Chapter 4 of ACLH. Roughly speaking, in that chapter, we present our logic)
153 W( \050the)152 W
9504 49740 MT
(Boyer-Moore Logic or NQTHM Logic, as it is sometimes known\051 by)
238 W( starting from)239 W
9504 51026 MT
(standard first order logic as in)
115 W( [70])
SH( and then)
115 W( adding some axioms that describe certain)114 W
9504 52312 MT
(data structures, including the integers, ordered)
137 W( pairs, and symbols. We include in the)138 W
9504 53598 MT
(logic a principle of definition for recursive functions over)
38 W( these data structures. Among)37 W
9504 54884 MT
(our rules of inference is a schema for proof by induction.)
20 W( This)
342 W( schema would be merely)21 W
9504 56170 MT
(a derived rule of inference were we to cast our induction axioms in the traditional form.)SH
9504 58742 MT
(The syntax of our logic is close to that of Lisp. In fact, from the time we)
24 W( started writing)23 W
9504 60028 MT
(our prover)
115 W( [9])
SH( we have regarded it as a theorem prover for a)
115 W( theory of Lisp functions.)116 W
9504 61314 MT
(Some of the earliest theorems we proved mechanically were inspired by some)
330 W( of)329 W
9504 62600 MT
(McCarthy's seminal papers on the logic of)
20 W( Lisp, including)
21 W( [54], [56],)
SH( and)
21 W( [58].)
SH( Because)342 W
9504 63886 MT
(Lisp may be viewed as both a)
7 W( logic and a programming language, we have always found)6 W
9504 65172 MT
(it a)
198 W( most natural setting in which to express theorems about computations and other)199 W
9504 66458 MT
(parts of constructive mathematics.)SH
9504 69030 MT
(Both the axioms of the NQTHM)
164 W( logic and the conjectures it entertains are quantifier)163 W
9504 70316 MT
(free, or, more precisely, implicitly universally quantified ``on the far outside.'')
68 W( In)
438 W( fact,)69 W
9504 71602 MT
(NQTHM does not include rules for)
82 W( manipulating quantifiers at all. However, by using)81 W
ES
%%Page: 3 4
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(3)SH
12 SS
9504 8023 MT
(recursive functions, we are able to express many of)
18 W( the things that one usually expresses)19 W
9504 9309 MT
(with quantifiers when dealing with ``finite'')
269 W( objects such as trees of integers. For)268 W
9504 10595 MT
(example, to state and prove the)
135 W( uniqueness and existence of prime factorizations)
136 W( [11],)SH
9504 11881 MT
(we define recursive functions which factor integers)
194 W( and which compute whether two)193 W
9504 13167 MT
(finite sequences of integers are permutations of one another. This practice of using)207 W
9504 14453 MT
(recursive functions to do work one might do with quantifiers may have been)
66 W( originated)65 W
9504 15739 MT
(by Skolem in)
40 W( [71],)
SH( who was perhaps the earliest to demonstrate that arithmetic)
40 W( could be)41 W
9504 17025 MT
(built up using)
33 W( entirely constructive methods. Skolem's program is further carried out in)32 W
9804 18311 MT
([34].)SH
9504 20883 MT
(Here is an example of a)
81 W( definition that one might give to the prover for a function that)82 W
9504 22169 MT
(appends, i.e. concatenates, two lists:)SH
10 /Courier-Bold AF
11304 23974 MT
(Definition.)SH
11304 25105 MT
(\050APP X Y\051)SH
13104 26236 MT
(=)SH
11304 27367 MT
(\050IF \050LISTP X\051)SH
13704 28498 MT
(\050CONS \050CAR X\051 \050APP \050CDR X\051 Y\051\051)SH
13704 29629 MT
(Y\051)SH
12 /Times-Roman AF
9504 31583 MT
(In rough English, this definition says that to append a)
28 W( list)27 W
/Courier-Bold SF
37552 XM
(X)SH
/Times-Roman SF
38599 XM
(to a list)27 W
/Courier-Bold SF
42516 XM
(Y)SH
/Times-Roman SF
(, if)27 W
/Courier-Bold SF
44924 XM
(X)SH
/Times-Roman SF
45971 XM
(is nonemtpy,)27 W
9504 32869 MT
(then construct \050i.e.)10 W
/Courier-Bold SF
18769 XM
(CONS)SH
/Times-Roman SF
(\051 the)
10 W( list whose first element is the first element of)11 W
/Courier-Bold SF
46211 XM
(X)SH
/Times-Roman SF
(, i.e.)11 W
/Courier-Bold SF
49320 XM
(\050CAR)SH
9504 34155 MT
(X\051)SH
/Times-Roman SF
11303 XM
(, and whose other elements are the)
59 W( result of appending the rest of)58 W
/Courier-Bold SF
43599 XM
(X)SH
/Times-Roman SF
(, i.e.)58 W
/Courier-Bold SF
46802 XM
(\050CDR X\051)58 W
/Times-Roman SF
(,)SH
9504 35441 MT
(and)SH
/Courier-Bold SF
11537 XM
(Y)SH
/Times-Roman SF
(. On)
300 W( the other hand, if)SH
/Courier-Bold SF
23424 XM
(X)SH
/Times-Roman SF
24444 XM
(is empty, just return)SH
/Courier-Bold SF
34348 XM
(Y)SH
/Times-Roman SF
(.)SH
9504 38013 MT
(A simple example of a theorem that one might)
21 W( ask NQTHM to prove is the associativity)22 W
9504 39299 MT
(of)SH
/Courier-Bold SF
10804 XM
(APP)SH
/Times-Roman SF
(, which one would state as)SH
10 /Courier-Bold AF
11304 41104 MT
(Theorem.)SH
11304 42235 MT
(\050APP \050APP X Y\051 Z\051 = \050APP X \050APP Y Z\051\051)SH
12 /Times-Roman AF
9504 44189 MT
(We discuss a proof of this theorem below when we describe the induction heuristic.)SH
14 /Times-Bold AF
9504 46559 MT
(3 The)
700 W( Prover)SH
13 SS
9504 48862 MT
(3.1 How)
650 W( to Get a Copy)SH
12 /Times-Roman AF
9504 51029 MT
(NQTHM is a)
264 W( Common Lisp program whose source files require about one million)263 W
9504 52315 MT
(characters. NQTHM)
798 W( runs in a variety of)
249 W( Common Lisps including Lucid, Allegro,)250 W
9504 53601 MT
(Symbolics, and KCL.)
94 W( It)
487 W( is publicly available, but a license is now required. We have)93 W
9504 54887 MT
(recently started to require a license to keep track of copies)
119 W( at the strong suggestion of)120 W
9504 56173 MT
(one of our sponsors. We previously distributed the same code)
202 W( without copyright or)201 W
9504 57459 MT
(license. At)
410 W( the time of this writing,)
55 W( a copy may be obtained without fee by anonymous)56 W
9504 58745 MT
(ftp from Internet site cli.com \050start with)
52 W( the file /pub/nqthm/README\051 or on tape for a)51 W
9504 60031 MT
(modest fee by writing to the authors at Computational Logic, 1717 W. 6th St.,)
99 W( Austin,)100 W
9504 61317 MT
(Texas 78703. The currently released version of NQTHM was first released in July of)114 W
9504 62603 MT
(1988, and no bugs affecting soundness have been)
30 W( reported as of the time of this writing.)31 W
9504 63889 MT
(The chapter of ACLH on installation describes in complete detail how to)
261 W( bring up)260 W
9504 65175 MT
(NQTHM from the sources.)SH
ES
%%Page: 4 5
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(4)SH
13 /Times-Bold AF
9504 8071 MT
(3.2 WARNING:)
650 W( Difficulty)
325 W( of Use)SH
12 /Times-Roman AF
9504 10238 MT
(It is hard, perhaps impossible, to use NQTHM effectively without)
7 W( investing a substantial)8 W
9504 11524 MT
(amount of time learning how to use it. To avoid)
178 W( disappointment, a prospective user)177 W
9504 12810 MT
(should probably be prepared first)
13 W( to understand most of two rather long books, ACL and)14 W
9504 14096 MT
(ACLH. Almost)
442 W( all of the successful users of NQTHM)
71 W( have in fact also taken a course)70 W
9504 15382 MT
(from us at the University of Texas at Austin)
103 W( on proving theorems in our logic. Based)104 W
9504 16668 MT
(upon teaching)
67 W( related courses at Stanford, our former student N. Shankar advises that a)66 W
9504 17954 MT
(user unfamiliar with the heuristics employed in the prover, as)
13 W( described in great detail in)14 W
9504 19240 MT
(ACL, is very unlikely to direct the prover to prove anything significant.)
307 W( Besides)912 W
9504 20526 MT
(precisely describing the logic of NQTHM, ACLH)
313 W( also serves as a user's manual,)314 W
9504 21812 MT
(describing in great detail all of the commands with which one can direct the prover.)SH
13 /Times-Bold AF
9504 24027 MT
(3.3 Heuristic)
650 W( Character of NQTHM)SH
12 /Times-Roman AF
9504 26194 MT
(NQTHM is a)226 W
/Times-Italic SF
16814 XM
(heuristic)SH
/Times-Roman SF
21542 XM
(theorem-prover. By)
750 W( heuristic, we mean that we have coded)225 W
9504 27480 MT
(guessing strategies for searching through)
147 W( the space of possible proofs for conjectures.)148 W
9504 28766 MT
(For example, NQTHM guesses when it is best to)
48 W( cut off ``back chaining''. If the guess)47 W
9504 30052 MT
(is wrong, which it can easily be, then)
172 W( no proof may be found. As another example,)173 W
9504 31338 MT
(NQTHM often guesses an induction to try, when all other proof techniques)
76 W( cease to be)75 W
9504 32624 MT
(applicable. If)
627 W( the guess is wrong, then NQTHM will irrevocably go chasing down a)164 W
9504 33910 MT
(search path that is probably totally fruitless. On the other hand, because NQTHM does)59 W
9504 35196 MT
(have heuristics, NQTHM is able to find proofs for what)
204 W( we believe is a remarkable)205 W
9504 36482 MT
(number of theorems. One crude measure of the effectiveness of)
131 W( NQTHM is that it is)130 W
9504 37768 MT
(always is able to make an above average grade on the final examinations we give to)
35 W( our)36 W
9504 39054 MT
(students in an introductory graduate course on proving theorems in the NQTHM logic.)SH
9504 41626 MT
(We were inspired in part to build a theorem prover that is heuristic by the success)
139 W( of)138 W
9504 42912 MT
(W. W. Bledsoe)
241 W( [4], [5])
SH( in writing)
241 W( such theorem provers, including one that guessed)242 W
9504 44198 MT
(inductions based upon the terms in the conjecture. One of the)
153 W( major concerns in the)152 W
9504 45484 MT
(literature on automated)
183 W( reasoning in the 60's and 70's was with the completeness of)184 W
9504 46770 MT
(proof procedures. NQTHM)
381 W( is certainly not complete, except when guided by a)380 W
9504 48056 MT
(knowledgeable user.)SH
13 /Times-Bold AF
9504 50271 MT
(3.4 Induction)650 W
12 /Times-Roman AF
9504 52438 MT
(Perhaps the most important heuristic in NQTHM is)
70 W( the induction heuristic. The key to)71 W
9504 53724 MT
(the success of our induction heuristic is that it is)
14 W( closely tied to the principle of recursive)13 W
9504 55010 MT
(definition which we employ. For example, to prove the associativity of)15 W
/Courier-Bold SF
44357 XM
(APP)SH
/Times-Roman SF
(, mentioned)15 W
9504 56296 MT
(above, NQTHM would guess to induction on)130 W
/Courier-Bold SF
32414 XM
(X)SH
/Times-Roman SF
33564 XM
(by)SH
/Courier-Bold SF
35194 XM
(CDR)SH
/Times-Roman SF
(, i.e. by the length of the)
130 W( first)129 W
9504 57582 MT
(argument. This)
436 W( induction mirrors the way)
68 W( that)69 W
/Courier-Bold SF
32755 XM
(APP)SH
/Times-Roman SF
35284 XM
(recurses. An)
438 W( important part of the)69 W
9504 58868 MT
(induction heuristic is)
44 W( filtering out suggested inductions which are ``not likely'' to work,)43 W
9504 60154 MT
(such as the induction on)SH
/Courier-Bold SF
21406 XM
(Y)SH
/Times-Roman SF
22426 XM
(by)SH
/Courier-Bold SF
23926 XM
(CDR)SH
/Times-Roman SF
26386 XM
(in the theorem above.)SH
9504 62726 MT
(The NQTHM practice of not)
240 W( permitting quantification but of permitting the user to)241 W
9504 64012 MT
(define recursive functions to express what)
36 W( might otherwise require quantification has an)35 W
9504 65298 MT
(effect of)
48 W( forcing the user to hint implicitly how to prove conjectures: try inductions that)49 W
9504 66584 MT
(mirror the definitions of the recursive functions used in the conjectures.)
4 W( This)
306 W( heuristic is)3 W
9504 67870 MT
(startlingly successful for the NQTHM logic.)SH
ES
%%Page: 5 6
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(5)SH
13 /Times-Bold AF
9504 8071 MT
(3.5 Simplification)650 W
12 /Times-Roman AF
9504 10238 MT
(Besides induction, the other most important)
68 W( theorem proving component in NQTHM is)69 W
9504 11524 MT
(the simplifier. The simplifier combines rewriting \050cf.)
278 W( [74])
SH( and)
277 W( [4]\051)
SH( with linear and)277 W
9504 12810 MT
(binary resolution and subsumption)
180 W( \050cf.)
181 W( [65])
SH( and)
181 W( [53]\051.)
SH( The)
662 W( simplifier also includes a)181 W
9504 14096 MT
(semi-decision procedure for a part of arithmetic, based upon ideas in [36].)SH
9504 16668 MT
(An aspect of our simplifier that)
111 W( accounts for much of its effectiveness is a ``type set'')110 W
9504 17954 MT
(facility which keeps track, for each expression actively)
308 W( under consideration, a bit-)309 W
9504 19240 MT
(mask's worth)
186 W( of information indicating a conservative estimate of the ``type'' of the)185 W
9504 20526 MT
(expression in terms of the basic data types of the NQTHM)
317 W( Logic. The type set)318 W
9504 21812 MT
(procedure, like most of the current simplifier, is described in ACL.)SH
13 /Times-Bold AF
9504 24027 MT
(3.6 Other)
650 W( Heuristics)SH
12 /Times-Roman AF
9504 26194 MT
(Of considerably less significance)
103 W( than induction or simplification are various NQTHM)102 W
9504 27480 MT
(routines which are named)
652 W( ``elimination of destructors,'' ``cross fertilization,'')653 W
9504 28766 MT
(``generalization,''and ``elimination of irrelevance.'' The structure)
73 W( of NQTHM, at least)72 W
9504 30052 MT
(as it was in 1979, is described in complete detail in ACL. That work)
62 W( remains a largely)63 W
9504 31338 MT
(accurate description of NQTHM except for \050a\051 the integration of the arithmetic decision)41 W
9504 32624 MT
(procedure, described in)
499 W( [19],)
SH( \050b\051 the addition of metafunctions and)
499 W( an efficient)500 W
9504 33910 MT
(representation for large constant terms, described in)
20 W( [12],)
SH( \050c\051 some simplifications of the)20 W
9504 35196 MT
(induction machinery that have never been)
226 W( documented, \050d\051 the axiomatization of an)227 W
9504 36482 MT
(interpreter for partial recursive functions)
145 W( [20],)
SH( and \050e\051)
145 W( an implementation of a derived)144 W
9504 37768 MT
(rule of inference called ``functional instantiation'' [8].)SH
14 /Times-Bold AF
9504 40138 MT
(4 The)
700 W( Importance of the User in Finding Proofs)SH
12 /Times-Roman AF
9504 42393 MT
(Although NQTHM is quite capable of finding proofs for some simple)
174 W( theorems with)175 W
9504 43679 MT
(which even)
153 W( graduate students may struggle, we think of NQTHM as more of a proof)152 W
9504 44965 MT
(checker than as a theorem-prover. What do we)
74 W( mean by this distinction? It is perhaps)75 W
9504 46251 MT
(not possible to spell out clearly what the distinction is. However,)
53 W( whenever we have in)52 W
9504 47537 MT
(mind an interesting theorem for NQTHM to prove, we almost always expect to)
66 W( have to)67 W
9504 48823 MT
(suggest to NQTHM what)
127 W( the main intermediate steps to the proof are. We do expect)126 W
9504 50109 MT
(NQTHM to do a great)
28 W( deal of tedious work filling in minor details. And when filling in)29 W
9504 51395 MT
(such minor details, NQTHM very often exposes minor oversights)
155 W( in our statement of)154 W
9504 52681 MT
(theorems. The)
470 W( situation is entirely different for some ``real theorem-provers,'')
85 W( such as)86 W
9504 53967 MT
(those of Wu and Chou)
112 W( [27],)
SH( which one)
112 W( expects to decide quickly any theorem in their)111 W
9504 55253 MT
(domain.)SH
9504 57825 MT
(The earliest version of NQTHM)
13 W( [9])
SH( had no facility for user guidance. The power of)
13 W( that)14 W
9504 59111 MT
(early version of the prover may be very crudely)
146 W( characterized by saying that, starting)145 W
9504 60397 MT
(from Peano's axioms, and analogous)
329 W( axioms for lists, the prover could not prove)330 W
9504 61683 MT
(anything much more difficult than the)
96 W( associativity of multiplication or the correctness)95 W
9504 62969 MT
(of an insertion sort algorithm.)SH
9504 65541 MT
(In order to)
14 W( permit NQTHM to prove theorems harder than these \050without ``cheating'' by)15 W
9504 66827 MT
(adding additional)
110 W( formulas as axioms\051, the most important step we took was to permit)109 W
9504 68113 MT
(the user to suggest ``lemmas,'' i.e.)
79 W( intermediate theorems, which would first be proved)80 W
9504 69399 MT
(by NQTHM and then made available)
295 W( for use in subsequent proofs, mainly by the)294 W
9504 70685 MT
(simplifier [10].)
SH( Permitting)
708 W( the use of lemmas on the one)
204 W( hand makes NQTHM feel)205 W
9504 71971 MT
(more like a proof checker than a theorem prover, but on)
129 W( the other hand it permits the)128 W
ES
%%Page: 6 7
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(6)SH
12 SS
9504 8023 MT
(checking of a very substantial part of elementary number theory)
175 W( [66],)
SH( even including)175 W
9504 9309 MT
(Gauss's law of quadratic)
317 W( reciprocity \050the crown jewel of number theory\051, and the)316 W
9504 10595 MT
(correctness of some interesting algorithms [16].)SH
14 /Times-Bold AF
9504 12965 MT
(5 Our)
700 W( Motivation: Computer System Correctness)SH
12 /Times-Roman AF
9504 15220 MT
(Given that NQTHM is not)
50 W( a very ``smart'' theorem prover, one might well ask why we)51 W
9504 16506 MT
(have kept working on it for so)
98 W( many years! Our main motivation has been to develop)97 W
9504 17792 MT
(NQTHM into a system that can be used in a practical way to check the)
110 W( correctness of)111 W
9504 19078 MT
(computer systems, thereby reducing the frequency of bugs in computer programs.)SH
9504 21650 MT
(The idea)
393 W( of proving the correctness of algorithms is at least as old as Euclid's)392 W
9504 22936 MT
(demonstration of the correctness of an algorithm for finding the)
326 W( greatest common)327 W
9504 24222 MT
(divisor of two integers)
75 W( [29].)
SH( The)
450 W( idea of correctness proofs is also clearly stated)
75 W( in the)74 W
9504 25508 MT
(classic papers of Goldstine and von Neumann)
77 W( [73])
SH( that describe the first)
77 W( von Neumann)78 W
9504 26794 MT
(machine and how to)
109 W( use it. In those papers fifteen programs, including a sort routine,)108 W
9504 28080 MT
(are specified, coded in machine)
196 W( language, and proved correct. Although correctness)197 W
9504 29366 MT
(proofs were)
174 W( undoubtedly constructed by many early programmers, publications about)173 W
9504 30652 MT
(this idea seem rare until the 60s, when McCarthy)
269 W( [56],)
SH( Floyd)
269 W( [30],)
SH( Hoare)
269 W( [35],)
SH( and)270 W
9504 31938 MT
(Burstall [26])
SH( described means for proving the correctness of programs)
63 W( written in higher)62 W
9504 33224 MT
(level languages. Subsequently a rather sizable literature on the subject has developed.)SH
9504 35796 MT
(Proofs of the)
165 W( correctness of computing systems seem to be much longer, much more)166 W
9504 37082 MT
(tedious, and much more error prone than proofs in ordinary)
419 W( mathematics. The)418 W
9504 38368 MT
(additional length is due to the fact that the computing systems may)
291 W( easily require)292 W
9504 39654 MT
(hundreds of)
15 W( pages of specification, whereas most propositions in mathematics can easily)14 W
9504 40940 MT
(be stated in a few pages -- even if one includes the axiomatization of set theory,)295 W
9504 42226 MT
(analysis, and algebra. The tediousness and error level are perhaps due)
22 W( to this length and)21 W
9504 43512 MT
(also to the fact that many parts of computing systems are mathematically boring.)SH
9504 46084 MT
(The idea of)
18 W( mechanically checking proofs of correctness of computing systems has been)19 W
9504 47370 MT
(pursued by many researchers, e.g. those mentioned in the)
111 W( review article)
110 W( [7].)
SH( Research)520 W
9504 48656 MT
(on this topic has grown to the extent that there are several research laboratories \050e.g.)
14 W( the)329 W
9504 49942 MT
(Computer Science Laboratory of SRI International\051)
143 W( and several small companies \050e.g.)142 W
9504 51228 MT
(our own Computational Logic, Inc. and Richard Platek's Odyssey Associates, Inc.\051)276 W
9504 52514 MT
(which devote a major portion of their efforts to research on this topic.)SH
14 /Times-Bold AF
9504 54884 MT
(6 Applications)700 W
12 /Times-Roman AF
9504 57139 MT
(We and others have used NQTHM to check the correctness of many)
146 W( small programs.)145 W
9504 58425 MT
(However, after many years of effort, we are beginning to)
169 W( see mechanical correctness)170 W
9504 59711 MT
(proofs of entire small computing systems.)
148 W( By)
595 W( far, the most significant application of)147 W
9504 60997 MT
(NQTHM has been to a prove the correctness of a computing system known as)
84 W( the)85 W
/Times-Italic SF
50333 XM
(CLI)SH
9504 62283 MT
(Stack)SH
/Times-Roman SF
(, which includes)
373 W( \050a\051 a microprocessor design \050FM8502\051 based on gates and)372 W
9504 63569 MT
(registers [38],)
SH( \050b\051 an assembler \050Piton\051)
85 W( [61])
SH( that targets FM8502, and \050c\051)
85 W( a higher level)86 W
9504 64855 MT
(language \050micro Gypsy\051)
420 W( [76])
SH( that targets Piton. We have also seen a proof of)420 W
9504 66141 MT
(correctness of a small operating system kernel \050KIT\051)
42 W( [2].)
SH( Except)
384 W( for the)
42 W( Piton work, all)43 W
9504 67427 MT
(of these projects represent Ph.D. dissertations in computer science)
48 W( which we supervised)47 W
9504 68713 MT
(at the University of Texas. FM8502, Piton, micro Gypsy, and Kit are documented)
135 W( in)136 W
9504 69999 MT
(one place, a special issue of the)SH
/Times-Italic SF
24905 XM
(Journal of Automated Reasoning)SH
/Times-Roman SF
41040 XM
([62].)SH
ES
%%Page: 7 8
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(7)SH
12 SS
9504 8023 MT
(Another major application of NQTHM)
326 W( is the Ph.D. work of N. Shankar in proof)325 W
9504 9309 MT
(checking Godel's incompleteness theorem)
35 W( [69].)
SH( The)
370 W( text of this proof)
35 W( effort is included)36 W
9504 10595 MT
(in the standard distribution)
89 W( of NQTHM, along with Shankar's checking of the Church-)88 W
9504 11881 MT
(Rosser theorem.)SH
9504 14453 MT
(On pp. 4-9 of)
199 W( ACLH, we enumerate many other applications of NQTHM, including)200 W
9504 15739 MT
(those in list processing, elementary number theory, metamathematics, set theory, and)182 W
9504 17025 MT
(concurrent algorithms.)
226 W( Descriptions)
753 W( of some of these applications may be found in)227 W
9804 18311 MT
([16, 66, 12, 21, 17, 67], [68, 69, 20, 60, 28, 51, 37, 52], [13, 14, 15, 22, 77],)
SH( and)
199 W( also in)198 W
9804 19597 MT
([1, 31, 32, 33, 40, 75, 3], [48, 44, 41, 42], [39, 45, 23, 24, 25].)SH
9504 22169 MT
(Recently colleagues of ours at Computational Logic, Inc., Bill Young and Bill Bevier,)113 W
9504 23455 MT
(have used NQTHM to construct mechanically checked proofs of)
127 W( properties relating to)126 W
9504 24741 MT
(fault-tolerance. A)
374 W( key problem)
37 W( facing the designers of systems which attempt to ensure)38 W
9504 26027 MT
(fault tolerance by redundant processing)
164 W( is how to guarantee that the processors reach)163 W
9504 27313 MT
(agreement, even when one or more processing units are faulty.)
23 W( This)
347 W( problem, called the)24 W
9504 28599 MT
(Byzantine Generals problem)
160 W( or the problem of achieving)159 W
/Times-Italic SF
38447 XM
(interactive consistency)159 W
/Times-Roman SF
(, was)159 W
9504 29885 MT
(posed and solved by Pease, Shostak, and Lamport)
313 W( [64, 50].)
SH( They)
928 W( proved that the)314 W
9504 31171 MT
(problem is solvable if and)
31 W( only if the total number of processors exceeds three times the)30 W
9504 32457 MT
(number of faulty processors and devised an extremely clever algorithm \050the)
284 W( ``Oral)285 W
9504 33743 MT
(Messages'' Algorithm\051 which implements a solution to)
127 W( this problem. Bill Young and)126 W
9504 35029 MT
(Bill Bevier, have just finished developing a machine)
22 W( checked proof of the correctness of)23 W
9504 36315 MT
(this algorithm using NQTHM.)SH
9504 38887 MT
(Matt Kaufmann, of Computational)
463 W( Logic, Inc., has made extensive additions to)462 W
9504 40173 MT
(NQTHM, building a system called)
187 W( ``PC-NQTHM'' on top of NQTHM, which many)188 W
9504 41459 MT
(find more convenient than NQTHM for checking proofs. Information about PC-)354 W
9504 42745 MT
(NQTHM and some extensions and applications)
1310 W( may be found in)1311 W
9804 44031 MT
([46, 49, 45, 47, 63, 43, 76].)
SH( Among)
626 W( the theorems which)
163 W( Kaufmann has checked with)162 W
9504 45317 MT
(PC-NQTHM are:)SH
/Symbol SF
12252 47020 MT
(\267)SH
/Times-Roman SF
13104 XM
(Ramsey's theorem for exponent 2 \050both finite and infinite)
92 W( versions\051, with)93 W
13104 48306 MT
(explicit bound in the finite case [41, 46].)SH
/Symbol SF
12252 50335 MT
(\267)SH
/Times-Roman SF
13104 XM
(Correctness of an algorithm of Gries for finding the)
54 W( largest ``true square'')53 W
13104 51621 MT
(submatrix of a boolean matrix [40].)SH
/Symbol SF
12252 53650 MT
(\267)SH
/Times-Roman SF
13104 XM
(The Cantor-Schroeder-Bernstein theorem [46].)SH
/Symbol SF
12252 55679 MT
(\267)SH
/Times-Roman SF
13104 XM
(The correctness of a Towers of Hanoi program.)SH
/Symbol SF
12252 57708 MT
(\267)SH
/Times-Roman SF
13104 XM
(The irrationality of the square root of 2.)SH
/Symbol SF
12252 59737 MT
(\267)SH
/Times-Roman SF
13104 XM
(Correctness of a finite version of the collapsing function of Cohen forcing.)SH
14 /Times-Bold AF
9504 62107 MT
(7 Work)
700 W( in Progress: ACL2)SH
12 /Times-Roman AF
9504 64362 MT
(We are currently constructing an entirely)
99 W( new version of our prover. The name of the)100 W
9504 65648 MT
(new system is)155 W
/Times-Italic SF
17004 XM
(A Computational Logic for Applicative)
155 W( Common Lisp)154 W
/Times-Roman SF
(, which might be)154 W
9504 66934 MT
(abbreviated as ``ACL ACL'' but which we abbreviate as)
61 W( ``ACL2''. Whereas NQTHM)62 W
9504 68220 MT
(has been available for some time, extensively documented, and)
133 W( widely used, ACL2 is)132 W
9504 69506 MT
(still very much under development. Hence the following remarks are)
378 W( somewhat)379 W
9504 70792 MT
(speculative.)SH
ES
%%Page: 8 9
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(8)SH
12 SS
9504 8023 MT
(Instead of supporting ``Boyer-Moore logic'', which)
33 W( reflects an odd mixture of functions)32 W
9504 9309 MT
(vaguely, but not consistently, related to Lisp 1.5 and Interlisp,)
107 W( ACL2 directly supports)108 W
9504 10595 MT
(perfectly and accurately \050we hope\051 a large subset of applicative Common)
45 W( Lisp. That is,)44 W
9504 11881 MT
(ACL2 is to applicative Common Lisp)
68 W( what NQTHM is to the ``Boyer-Moore logic'', a)69 W
9504 13167 MT
(programming/theorem proving environment for an executable logic of recursive)528 W
9504 14453 MT
(functions.)SH
9504 17025 MT
(More precisely,)
468 W( we have identified an applicative subset of Common Lisp and)469 W
9504 18311 MT
(axiomatized it, following Steele's)
477 W( [72])
SH( carefully.)
477 W( Because)
1253 W( arrays, property lists,)476 W
9504 19597 MT
(input/output and certain other commonly used programming features are)
142 W( not provided)143 W
9504 20883 MT
(applicatively in)
10 W( Common Lisp \050i.e., they all involve the notion of explicit state changes\051,)9 W
9504 22169 MT
(we axiomatized)
447 W( applicative versions of these features. For example, when one)448 W
9504 23455 MT
(``changes'' an array object, one gets a new array object.)
248 W( However,)
795 W( we gave these)247 W
9504 24741 MT
(applicative functions very efficient implementations which are in)
154 W( complete agreement)155 W
9504 26027 MT
(with their axiomatic descriptions but which happen to execute at near von Neumann)191 W
9504 27313 MT
(speeds when used in the normal von Neumann style \050in which ``old'' versions)
216 W( of a)217 W
9504 28599 MT
(modified structure are not accessed\051. The result is ``applicative Common Lisp'')
77 W( which)76 W
9504 29885 MT
(is also an executable mathematical logic.)SH
9504 32457 MT
(Like NQTHM, the logic of applicative Common Lisp provides a)
117 W( definitional principle)118 W
9504 33743 MT
(that permits)
397 W( the sound extension of the system via the introduction of recursive)396 W
9504 35029 MT
(functions. Unlike)
619 W( NQTHM, however, functions in applicative Common Lisp may be)160 W
9504 36315 MT
(defined only on a subset of the universe.)
169 W( Like)
637 W( NQTHM, the new logic provides the)168 W
9504 37601 MT
(standard first order rules)
50 W( of inference and induction. However, the axioms are different)51 W
9504 38887 MT
(since, for example, NQTHM and ACL2 differ on what)399 W
/Courier-Bold SF
39659 XM
(\050CAR NIL\051)398 W
/Times-Roman SF
47235 XM
(is. Most)1096 W
9504 40173 MT
(importantly for the current purposes, we claim that all)
4 W( correct Common Lisps implement)5 W
9504 41459 MT
(applicative Common Lisp directly and that, unlike)
488 W( NQTHM's logic, applicative)487 W
9504 42745 MT
(Common Lisp is a practical programming language.)SH
9504 45317 MT
(ACL2 is a theorem prover)
517 W( and programming/proof environment for applicative)518 W
9504 46603 MT
(Common Lisp. ACL2 includes all)
19 W( of the functionality of NQTHM \050as understood in the)18 W
9504 47889 MT
(new setting\051 plus many new)
193 W( features \050e.g., congruence-based rewriting\051. The source)194 W
9504 49175 MT
(code for ACL2 consists of about 1.5 million characters, all but 43,000 of which)
104 W( are in)103 W
9504 50461 MT
(applicative Common Lisp. That is, 97% of ACL2 is written applicatively in the same)111 W
9504 51747 MT
(logic for which ACL2 proves theorems. The 3% of non-applicative)
95 W( code is entirely at)94 W
9504 53033 MT
(the top-level of the read-eval-print user interface and deals with)
17 W( reading user input, error)18 W
9504 54319 MT
(recovery and interrupts.)
27 W( We)
353 W( expect to implement)26 W
/Courier-Bold SF
33818 XM
(read)SH
/Times-Roman SF
37024 XM
(applicatively and limit the non-)26 W
9504 55605 MT
(applicative part)
73 W( of ACL2 to the essential interaction with the underlying Common Lisp)74 W
9504 56891 MT
(host system.)SH
9504 59463 MT
(Thus, in ACL2 as it currently stands, the definitional principle)
230 W( is implemented as a)229 W
9504 60749 MT
(function in logic, including the syntax checkers, error handlers,)
74 W( and data base handlers.)75 W
9504 62035 MT
(The entire ``Boyer-Moore theorem)
113 W( prover'' -- as that term is now understood to mean)112 W
9504 63321 MT
(``the theorem prover Boyer and Moore have written for ACL2'' -- is)
106 W( a function in the)107 W
9504 64607 MT
(logic, including the simplifiers, the decision procedures, the induction heuristics, and)
35 W( all)34 W
9504 65893 MT
(of the proof description generators.)SH
9504 68465 MT
(The fact that almost)
14 W( all of ACL2 is written applicatively in the same logic for which it is)15 W
9504 69751 MT
(a theorem prover allows the ACL2 source code)
350 W( to be among the axioms in that)349 W
9504 71037 MT
(definitional extension of)
77 W( the logic. The user of the ACL2 system can define functions,)78 W
ES
%%Page: 9 10
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(9)SH
12 SS
9504 8023 MT
(combine his functions with those of ACL2, execute)
14 W( them, or prove things about them, in)13 W
9504 9309 MT
(a unified setting.)
151 W( One)
603 W( need only understand one language, Common Lisp, to use the)152 W
9504 10595 MT
(``logic'', interact with the system, interface to the system, or modify the system.)346 W
9504 11881 MT
(DEFMACRO can be used to extend the syntax of the language, users)
9 W( can introduce their)10 W
9504 13167 MT
(own front-ends by programming within the logic,)
269 W( and all of the proof routines are)268 W
9504 14453 MT
(accessible to users and have exceptionally clear \050indeed, applicative\051)
90 W( interfaces. Many)91 W
9504 15739 MT
(new avenues in metatheoretic extensibility are waiting to)
105 W( be explored. We believe we)104 W
9504 17025 MT
(have taken a major step towards the goal of perhaps someday checking the soundness of)21 W
9504 18311 MT
(most of the theorem prover by defining the theorem prover in a formalized logic.)SH
9504 20883 MT
(At the time of this)
257 W( writing, we have completely recoded all of the functionality of)256 W
9504 22169 MT
(NQTHM, but have only begun)
105 W( experimentation with proving theorems. However, our)106 W
9504 23455 MT
(preliminary evidence is that there will be no substantial degradation in performance,)202 W
9504 24741 MT
(even though ACL2 is coded applicatively.)SH
14 /Times-Bold AF
9504 27111 MT
(8 Conclusions)700 W
13 SS
9504 29414 MT
(8.1 Proof)
650 W( Checking as a Mere Engineering Challenge)SH
12 /Times-Roman AF
9504 31581 MT
(In our)
3 W( view it seems humanly feasible to write mechanical proof checkers for any part of)4 W
9504 32867 MT
(mathematics and to check mechanically any result in)
233 W( mathematics. There has been)232 W
9504 34153 MT
(much doubt cast on the feasibility of formal proofs, even by such respected authorities)94 W
9504 35439 MT
(as Bourbaki [6])SH
11 SS
12459 37091 MT
(But formalized mathematics cannot in practice be)
21 W( written down in full, and therefore)20 W
11704 38287 MT
(we must have confidence in what might)
410 W( be called the common sense of the)411 W
11704 39483 MT
(mathematician ... We shall therefore very quickly abandon formalized mathematics ...)SH
12 SS
9504 42055 MT
(We believe that we have enough practical evidence to)
36 W( extrapolate that mechanical proof)35 W
9504 43341 MT
(checking any mathematical)
311 W( result is feasible, not some mere theoretical possibility)312 W
9504 44627 MT
(which would require a computer the size of the)
189 W( universe. We can make no definite)188 W
9504 45913 MT
(claim about the cost of doing such)
106 W( proof checking, given a suitable proof checker, but)107 W
9504 47199 MT
(we suspect that in the worst case)
131 W( it is somewhere between approximately ten and one)130 W
9504 48485 MT
(hundred times as expensive as)
101 W( doing careful hand proofs at the level of an upper level)102 W
9504 49771 MT
(undergraduate mathematics textbook. In a few areas of mathematics, such as)
230 W( those)229 W
9504 51057 MT
(described by)
340 W( [27])
SH( the cost is much less than doing careful hand proofs. We are)340 W
9504 52343 MT
(optimistic that research by top mathematicians will expand the areas)
490 W( in which)489 W
9504 53629 MT
(mechanical theorem-provers are better than most mathematicians.)SH
13 /Times-Bold AF
9504 55844 MT
(8.2 Checking)
650 W( the Correctness of Computing Systems)SH
12 /Times-Roman AF
9504 58011 MT
(Almost as a corollary to the)
183 W( preceding view, we assert that it is humanly feasible to)184 W
9504 59297 MT
(check mechanically the correctness)
155 W( of computer systems against formal specifications)154 W
9504 60583 MT
(for those systems. Moreover, we believe)
24 W( that the reliability of computing systems could)25 W
9504 61869 MT
(and should be increased significantly by)
272 W( requiring that critical systems be formally)271 W
9504 63155 MT
(specified and that their)
71 W( correctness with respect to those specifications be mechanically)72 W
9504 64441 MT
(checked. Again,)
500 W( we make no definite)
100 W( claim about the cost of doing such certification,)99 W
9504 65727 MT
(but given that, for example, there exist microprocessors that are in control)
158 W( of nuclear)159 W
9504 67013 MT
(weapons, we believe that the cost of doing such checking may well be less than)
33 W( the cost)32 W
9504 68299 MT
(of not doing such checking.)SH
ES
%%Page: 10 11
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(10)SH
13 /Times-Bold AF
9504 8071 MT
(8.3 Formalizing)
650 W( the Real World)SH
12 /Times-Roman AF
9504 10238 MT
(Although the correctness of)
12 W( algorithms and even systems is something that is reasonably)13 W
9504 11524 MT
(clearly understood from a)
146 W( mathematical point of view, it remains a major and largely)145 W
9504 12810 MT
(unexplored area of research to formalize the interactions of)
46 W( computing systems with the)47 W
9504 14096 MT
(``real world.'')
506 W( Even)
1311 W( correctly formalizing the behavior of a typical industrial)505 W
9504 15382 MT
(microcontroller, with its myriad)
101 W( timers, interrupts, buses, and A/D converters seems to)102 W
9504 16668 MT
(be on the edge of the state of the art of formalization.)
186 W( Any)
670 W( claim that a computing)185 W
9504 17954 MT
(system has been formally proved to interact safely with the world is no better than the)97 W
9504 19240 MT
(accuracy with which)
110 W( the behavior of the world has been formalized. The difficulty of)109 W
9504 20526 MT
(accurately formalizing the behavior of the world does not diminish the)
9 W( fact that typically)10 W
9504 21812 MT
(a very large part of what any computing system is)
283 W( supposed to do \050especially the)282 W
9504 23098 MT
(internal workings\051 can be formally specified, and that part is suitable for)
104 W( scrutiny with)105 W
9504 24384 MT
(formal, mechanical proof attempts.)SH
14 /Times-Bold AF
9504 26754 MT
(9 Acknowledgements)700 W
12 /Times-Roman AF
9504 29009 MT
(We want to express our thanks to a number)
7 W( of people who have contributed significantly)6 W
9504 30295 MT
(towards making NQTHM a successful prover.)SH
9504 32867 MT
(The first version of our prover was developed in)
122 W( the amazingly fertile environment of)123 W
9504 34153 MT
(Edinburgh University in the period 1971)
64 W( to 1974. While working in Bernard Meltzer's)63 W
9504 35439 MT
(Metamathematics Unit \050which then became)
165 W( the Department of Computational Logic\051,)166 W
9504 36725 MT
(we had the joy of working with such figures as J.A. Robinson,)
245 W( Bob Kowalski, Pat)244 W
9504 38011 MT
(Hayes, Alan Bundy, Aaron Sloman, and Woody Bledsoe. In nearby groups, such)
33 W( as the)34 W
9504 39297 MT
(Department of Machine Intelligence, we found inspiration from the likes of)
378 W( Rod)377 W
9504 40583 MT
(Burstall, Donald Michie,)
150 W( Robin Popplestone, Gordon Plotkin, Michael Gordon, Bruce)151 W
9504 41869 MT
(Anderson, David Warren, Raymond Aubin,)
87 W( Harry Barrow, John Darlington, and Julian)86 W
9504 43155 MT
(Davies. The)
440 W( time and place seemed to be embued with quiet inspiration. It is hard for)70 W
9504 44441 MT
(us to imagine that our prover could have put down its roots anyplace else.)SH
9504 47013 MT
(John McCarthy's)
56 W( influence on our work has been major. His invention of Lisp gave us)55 W
9504 48299 MT
(a language)
22 W( [55, 59])
SH( in which to write NQTHM. His papers on proof checking, e.g.)
23 W( [57],)SH
9504 49585 MT
(and the mathematical theory of computation)
43 W( [58])
SH( gave us incentive to write a)
43 W( prover for)42 W
9504 50871 MT
(program verification, reasoning techniques to)
41 W( encode, and sample theorems on which to)42 W
9504 52157 MT
(work. We)
480 W( have mentioned above Woody)
90 W( Bledsoe's influence on our work in showing)89 W
9504 53443 MT
(how to write heuristic theorem provers similar to ours.)SH
9504 56015 MT
(We thank Rod Burstall for his inspiring and elegant paper)
96 W( on structural induction)
97 W( [26].)SH
9504 57301 MT
(We thank Burstall, Michie, and Popplestone for use of the POP2 system running)
78 W( on an)77 W
9504 58587 MT
(ICL 4130 on which we coded the earliest version of our prover. POP2 is)
137 W( a Lisp-like)138 W
9504 59873 MT
(language with an Algol-like syntax and many features ahead of its time,)
277 W( including)276 W
9504 61159 MT
(streams and abstract data)
27 W( types, which influenced the design of the shell construct in the)28 W
9504 62445 MT
(NQTHM logic.)SH
9504 65017 MT
(At SRI International and Xerox PARC \050JSM\051, we translated)
146 W( our prover into Lisp and)145 W
9504 66303 MT
(made major extensions to it. We owe a debt of thanks to many people there for)
119 W( their)120 W
9504 67589 MT
(support and encouragement, including)
274 W( Robert W. Taylor, Warren Teitelmann, Peter)273 W
9504 68875 MT
(Deutsch, Butler Lampson, Jack Goldberg, Peter Neumann, Karl Levitt, Bernie)
136 W( Elspas,)137 W
9504 70161 MT
(Rob Shostak, Jay Spitzen, Les Lamport, Joe Goguen, Richard Waldinger, Nils Nilsson,)72 W
9504 71447 MT
(and Peter Hart.)SH
ES
%%Page: 11 12
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(11)SH
12 SS
9504 8023 MT
(We owe our user)
404 W( community a major debt. In particular, we acknowledge the)405 W
9504 9309 MT
(contributions of Bill Bevier, Bishop Brock, S.C. Chou, Ernie Cohen, Jimi Crawford,)196 W
9504 10595 MT
(David Goldschlag, C.H. Huang, Warren Hunt, Myung)
46 W( Kim, David Russinoff, Natarajan)47 W
9504 11881 MT
(Shankar, Mark Woodcock,)
144 W( Matt Wilding, Bill Young, and Yuan Yu. In addition, we)143 W
9504 13167 MT
(have profited enormously from our association with)
29 W( Matt Kaufmann, Hans Kamp, Chris)30 W
9504 14453 MT
(Lengauer, Norman Martin, John Nagle, Carl Pixley, and Bill Schelter. Topher)
94 W( Cooper)93 W
9504 15739 MT
(has the distinction of being the only)
61 W( person to have found an unsoundness in a released)62 W
9504 17025 MT
(version of our system.)SH
9504 19597 MT
(We also most gratefully acknowledge the support of our colleagues at the Institute for)112 W
9504 20883 MT
(Computing Science at the University of Texas, now)
68 W( almost all at Computational Logic,)69 W
9504 22169 MT
(especially Don Good and Sandy Olmstead who)
41 W( created and maintained at the Institute a)40 W
9504 23455 MT
(creative and relaxed research atmosphere with excellent)
123 W( computing facilities. In 1986)124 W
9504 24741 MT
(we moved our entire verification research group \050and its)
147 W( atmosphere\051 off campus and)146 W
9504 26027 MT
(established Computational Logic, Inc.)SH
9504 28599 MT
(Notwithstanding the contributions of all)
165 W( our friends and supporters, we would like to)166 W
9504 29885 MT
(make clear that NQTHM is a very large and complicated system)
292 W( that was written)291 W
9504 31171 MT
(entirely by the two of us. Not a single line of Lisp in our system was written by a)
46 W( third)47 W
9504 32457 MT
(party. Consequently,)
606 W( every bug in it)
153 W( is ours alone. Soundness is the most important)152 W
9504 33743 MT
(property of a theorem prover, and we urge any)
51 W( user who finds such a bug to report it to)52 W
9504 35029 MT
(us at once.)SH
9504 37601 MT
(The development of our logic and theorem prover has been an ongoing effort for)
13 W( the last)12 W
9504 38887 MT
(18 years. During that period we)
158 W( have received financial support from many sources.)159 W
9504 40173 MT
(Our work has been supported for over a decade by the National)
31 W( Science Foundation and)30 W
9504 41459 MT
(the Office of Naval Research. Of the many different grants and)
90 W( contracts involved we)91 W
9504 42745 MT
(list only the latest: NSF Grant DCR-8202943, NSF Grant DCR81-22039,)
236 W( and ONR)235 W
9504 44031 MT
(Contract N00014-81-K-0634. We are especially)
378 W( grateful to NSF, ONR, and our)379 W
9504 45317 MT
(technical monitors there, Tom Keenan, Bob Grafton, and Ralph Wachter,)
136 W( for years of)135 W
9504 46603 MT
(steady support and encouragement.)SH
9504 49175 MT
(The development)
126 W( of our prover is currently supported in part at Computational Logic,)127 W
9504 50461 MT
(Inc., by the Defense Advanced Research Projects Agency, ARPA Order 6082 and)
8 W( by the)7 W
9504 51747 MT
(Office of Naval Research, ONR Contract N00014-88-C-0454.)SH
9504 54319 MT
(We have received additional support over)
132 W( the years from the following sources, listed)133 W
9504 55605 MT
(chronologically: Science Research Council \050now the Science and)
59 W( Engineering Research)58 W
9504 56891 MT
(Council\051 of the United Kingdom, Xerox, SRI)
63 W( International, NASA, Air Force Office of)64 W
9504 58177 MT
(Scientific Research, Digital)
93 W( Equipment Corporation, the University of Texas at Austin,)92 W
9504 59463 MT
(the Venture Research Unit of British Petroleum, Ltd., and IBM.)SH
9504 62035 MT
(We thank Bill Schelter for the)
178 W( numerous suggestions he has made for improving the)179 W
9504 63321 MT
(performance of NQTHM under Austin-Kyoto Common Lisp.)SH
9504 65893 MT
(Thanks to Anne Boyer for editing this and other writings.)SH
9504 68465 MT
(Finally, we wish to)
364 W( express one negative acknowledgement. The research group)363 W
9504 69751 MT
(assembled at Edinburgh)
115 W( in the early 70's was scattered to the winds by the ``Lighthill)116 W
9504 71037 MT
(Report,'' the devastatingly negative review)
26 W( of artificial intelligence in Britain conducted)25 W
ES
%%Page: 12 13
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(12)SH
12 SS
9504 8023 MT
(by Sir James Lighthill.)
46 W( If)
394 W( computing becomes the dominant branch of both science and)47 W
9504 9309 MT
(engineering, as seems possible, we hope that renowned computer scientists, if asked,)181 W
9504 10595 MT
(will take the greatest care to review new developments in physics with humility, not)176 W
9504 11881 MT
(arrogance, and not attempt to quash new)
14 W( developments that do not fit into old paradigms)13 W
9504 13167 MT
(of science.)SH
ES
%%Page: 13 14
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(13)SH
15 /Times-Bold AF
27353 8205 MT
(References)SH
12 SS
9504 10944 MT
(1.)SH
/Times-Roman SF
11004 XM
(W. Bevier.)SH
/Times-Italic SF
16837 XM
(A Verified Operating System Kernel)SH
/Times-Roman SF
(. Ph.D.)
300 W( Th., University of Texas at)SH
9504 12230 MT
(Austin, 1987.)SH
/Times-Bold SF
9504 14339 MT
(2.)SH
/Times-Roman SF
11004 XM
(W. R. Bevier. "Kit and the Short Stack".)SH
/Times-Italic SF
31319 XM
(Journal of Automated Reasoning 5)SH
/Times-Roman SF
(, 4)SH
9504 15625 MT
(\0501989\051, 519-530.)SH
/Times-Bold SF
9504 17734 MT
(3.)SH
/Times-Roman SF
11004 XM
(William Bevier, Matt Kaufmann, and William Young. Translation of a Gypsy)SH
9504 19020 MT
(Compiler Example into the Boyer-Moore Logic. Internal Note 169, Computational)SH
9504 20306 MT
(Logic, Inc., January, 1990.)SH
/Times-Bold SF
9504 22415 MT
(4.)SH
/Times-Roman SF
11004 XM
(W.W. Bledsoe. "Splitting and Reduction Heuristics in Automatic Theorem Proving".)SH
/Times-Italic SF
9504 23701 MT
(Artificial Intelligence 2)SH
/Times-Roman SF
21009 XM
(\0501971\051, 55-77.)SH
/Times-Bold SF
9504 25810 MT
(5.)SH
/Times-Roman SF
11004 XM
(W. Bledsoe, R. Boyer, and W. Henneman. "Computer Proofs of Limit Theorems".)SH
/Times-Italic SF
9504 27096 MT
(Artificial Intelligence 3)SH
/Times-Roman SF
21009 XM
(\0501972\051, 27-60.)SH
/Times-Bold SF
9504 29205 MT
(6.)SH
/Times-Roman SF
11004 XM
(N. Bourbaki.)SH
/Times-Italic SF
17837 XM
(Elements of Mathematics.)SH
/Times-Roman SF
30872 XM
(Addison Wesley, Reading, Massachusetts,)SH
9504 30491 MT
(1968.)SH
/Times-Bold SF
9504 32600 MT
(7.)SH
/Times-Roman SF
11004 XM
(R. S. Boyer and J S. Moore. "Program Verification".)SH
/Times-Italic SF
37186 XM
(Journal of Automated)SH
9504 33886 MT
(Reasoning 1)SH
/Times-Roman SF
(, 1 \0501985\051, 17-23.)SH
/Times-Bold SF
9504 35995 MT
(8.)SH
/Times-Roman SF
11004 XM
(R. S. Boyer, D. M. Goldschlag, M. Kaufmann, and J S. Moore. Functional)SH
9504 37281 MT
(Instantiation in First Order Logic, Report 44. Computational Logic, 1717 W. 6th St.,)SH
9504 38567 MT
(Austin, Texas, 78703, U.S.A., 1989. To appear in the proceedings of the 1989)SH
9504 39853 MT
(Workshop on Programming Logic, Programming Methodology Group, University of)SH
9504 41139 MT
(Goteborg.)SH
/Times-Bold SF
9504 43248 MT
(9.)SH
/Times-Roman SF
11004 XM
(R. S. Boyer and J S. Moore. "Proving Theorems about LISP Functions".)SH
/Times-Italic SF
46621 XM
(JACM 22)SH
/Times-Roman SF
(,)SH
9504 44534 MT
(1 \0501975\051, 129-144.)SH
/Times-Bold SF
9504 46643 MT
(10.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. A Lemma Driven Automatic Theorem Prover for)SH
9504 47929 MT
(Recursive Function Theory. Proceedings of the 5th Joint Conference on Artificial)SH
9504 49215 MT
(Intelligence, 1977, pp. 511-519.)SH
/Times-Bold SF
9504 51324 MT
(11.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore.)SH
/Times-Italic SF
25671 XM
(A Computational Logic.)SH
/Times-Roman SF
37840 XM
(Academic Press, New York,)SH
9504 52610 MT
(1979.)SH
/Times-Bold SF
9504 54719 MT
(12.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. Metafunctions: Proving Them Correct and Using)SH
9504 56005 MT
(Them Efficiently as New Proof Procedures. In)SH
/Times-Italic SF
32404 XM
(The Correctness Problem in Computer)SH
9504 57291 MT
(Science)SH
/Times-Roman SF
(, R. S. Boyer and J S. Moore, Eds., Academic Press, London, 1981.)SH
/Times-Bold SF
9504 59400 MT
(13.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. A Verification Condition Generator for FORTRAN.)SH
9504 60686 MT
(In)SH
/Times-Italic SF
10804 XM
(The Correctness Problem in Computer Science)SH
/Times-Roman SF
(, R. S. Boyer and J S. Moore, Eds.,)SH
9504 61972 MT
(Academic Press, London, 1981.)SH
/Times-Bold SF
9504 64081 MT
(14.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. The Mechanical Verification of a FORTRAN Square)SH
9504 65367 MT
(Root Program. SRI International, 1981.)SH
/Times-Bold SF
9504 67476 MT
(15.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. MJRTY - A Fast Majority Vote Algorithm. Technical)SH
9504 68762 MT
(Report ICSCA-CMP-32, Institute for Computing Science and Computer Applications,)SH
9504 70048 MT
(University of Texas at Austin, 1982.)SH
ES
%%Page: 14 15
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(14)SH
12 /Times-Bold AF
9504 8023 MT
(16.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. "Proof Checking the RSA Public Key Encryption)SH
9504 9309 MT
(Algorithm".)SH
/Times-Italic SF
15896 XM
(American Mathematical Monthly 91)SH
/Times-Roman SF
(, 3 \0501984\051, 181-189.)SH
/Times-Bold SF
9504 11418 MT
(17.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. "A Mechanical Proof of the Unsolvability of the)SH
9504 12704 MT
(Halting Problem".)SH
/Times-Italic SF
18863 XM
(JACM 31)SH
/Times-Roman SF
(, 3 \0501984\051, 441-458.)SH
/Times-Bold SF
9504 14813 MT
(18.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore.)SH
/Times-Italic SF
25671 XM
(A Computational Logic Handbook.)SH
/Times-Roman SF
43139 XM
(Academic Press,)SH
9504 16099 MT
(New York, 1988.)SH
/Times-Bold SF
9504 18208 MT
(19.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. Integrating Decision Procedures into Heuristic)SH
9504 19494 MT
(Theorem Provers: A Case Study with Linear Arithmetic. In)SH
/Times-Italic SF
38607 XM
(Machine Intelligence 11)SH
/Times-Roman SF
(,)SH
9504 20780 MT
(Oxford University Press, 1988.)SH
/Times-Bold SF
9504 22889 MT
(20.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. "The Addition of Bounded Quantification and Partial)SH
9504 24175 MT
(Functions to A Computational Logic and Its Theorem Prover".)SH
/Times-Italic SF
40232 XM
(Journal of Automated)SH
9504 25461 MT
(Reasoning 4)SH
/Times-Roman SF
15771 XM
(\0501988\051, 117-172.)SH
/Times-Bold SF
9504 27570 MT
(21.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer and J S. Moore. A Mechanical Proof of the Turing Completeness of)SH
9504 28856 MT
(Pure Lisp. In)SH
/Times-Italic SF
16338 XM
(Automated Theorem Proving: After 25 Years)SH
/Times-Roman SF
(, W.W. Bledsoe and D.W.)SH
9504 30142 MT
(Loveland, Eds., American Mathematical Society, Providence, R.I., 1984, pp. 133-167.)SH
/Times-Bold SF
9504 32251 MT
(22.)SH
/Times-Roman SF
11604 XM
(R. S. Boyer, M. W. Green and J S. Moore. The Use of a Formal Simulator to)SH
9504 33537 MT
(Verify a Simple Real Time Control Program. In D. Gries, et. al, Ed.,)SH
/Times-Italic SF
42941 XM
(Beauty Is Our)SH
9504 34823 MT
(Business)SH
/Times-Roman SF
(, Springer, 1990. To Appear.)SH
/Times-Bold SF
9504 36932 MT
(23.)SH
/Times-Roman SF
11604 XM
(A. Bronstein and C. Talcott. String-Functional Semantics for Formal Verification)SH
9504 38218 MT
(of Synchronous Circuits, Report No. STAN-CS-88-1210. Computer Science)SH
9504 39504 MT
(Department, Stanford University, 1988.)SH
/Times-Bold SF
9504 41613 MT
(24.)SH
/Times-Roman SF
11604 XM
(A. Bronstein.)SH
/Times-Italic SF
18638 XM
(MLP: String-functional semantics and Boyer-Moore mechanization)SH
9504 42899 MT
(for the formal verification of synchronous circuits)SH
/Times-Roman SF
(. Ph.D.)
300 W( Th., Stanford University,)SH
9504 44185 MT
(1989.)SH
/Times-Bold SF
9504 46294 MT
(25.)SH
/Times-Roman SF
11604 XM
(A. Bronstein and C. Talcott. Formal Verification of Synchronous Circuits based on)SH
9504 47580 MT
(String-Functional Semantics: The 7 Paillet Circuits in Boyer-Moore. C-Cube 1989)SH
9504 48866 MT
(Workshop on Automatic Verification Methods for Finite State Systems. LNCS 407,)SH
9504 50152 MT
(1989, pp. 317-333.)SH
/Times-Bold SF
9504 52261 MT
(26.)SH
/Times-Roman SF
11604 XM
(R. Burstall. "Proving Properties of Programs by Structural Induction".)SH
/Times-Italic SF
46192 XM
(The)SH
9504 53547 MT
(Computer Journal 12)SH
/Times-Roman SF
(, 1 \0501969\051, 41-48.)SH
/Times-Bold SF
9504 55656 MT
(27.)SH
/Times-Roman SF
11604 XM
(S. Chou.)SH
/Times-Italic SF
16371 XM
(Mechancial Geometry Theorem Proving.)SH
/Times-Roman SF
36703 XM
(Reidel, 1988.)SH
/Times-Bold SF
9504 57765 MT
(28.)SH
/Times-Roman SF
11604 XM
(Benedetto Lorenzo Di Vito.)SH
/Times-Italic SF
25604 XM
(Verification of Communications Protocols and)SH
9504 59051 MT
(Abstract Process Models)SH
/Times-Roman SF
(. Ph.D.)
300 W( Th., University of Texas at Austin, 1982.)SH
/Times-Bold SF
9504 61160 MT
(29.)SH
/Times-Roman SF
11604 XM
(T. L. Heath \050translation and commentary\051.)SH
/Times-Italic SF
32539 XM
(The Thirteen Books of Euclid's)SH
9504 62446 MT
(Elements.)SH
/Times-Roman SF
14804 XM
(Dover, New York , 1908. p. 298, Vol 2., i.e. Proposition 2, Book VII.)SH
/Times-Bold SF
9504 64555 MT
(30.)SH
/Times-Roman SF
11604 XM
(R. Floyd. Assigning Meanings to Programs. In)SH
/Times-Italic SF
34942 XM
(Mathematical Aspects of Computer)SH
9504 65841 MT
(Science, Proceedings of Symposia in Applied Mathematics)SH
/Times-Roman SF
(, American Mathematical)SH
9504 67127 MT
(Society, Providence, Rhode Island, 1967, pp. 19-32.)SH
/Times-Bold SF
9504 69236 MT
(31.)SH
/Times-Roman SF
11604 XM
(David M. Goldschlag. "Mechanically Verifying Concurrent Programs with the)SH
9504 70522 MT
(Boyer-Moore Prover".)SH
/Times-Italic SF
20927 XM
(IEEE Transactions on Software Engineering)SH
/Times-Roman SF
42997 XM
(\050September 1990\051.)SH
9504 71808 MT
(To appear.)SH
ES
%%Page: 15 16
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(15)SH
12 /Times-Bold AF
9504 8023 MT
(32.)SH
/Times-Roman SF
11604 XM
(David M. Goldschlag. Mechanizing Unity. In)SH
/Times-Italic SF
34372 XM
(Proceedings of the IFIP TC2/WG2.3)SH
9504 9309 MT
(Working Conference on Programming Concepts and Methods)SH
/Times-Roman SF
(, M. Broy and C. B. Jones,)SH
9504 10595 MT
(Eds., Elsevier, Amsterdam, 1990.)SH
/Times-Bold SF
9504 12704 MT
(33.)SH
/Times-Roman SF
11604 XM
(David M. Goldschlag. "Proving Proof Rules: A Proof System for Concurrent)SH
9504 13990 MT
(Programs".)SH
/Times-Italic SF
15495 XM
(Compass '90)SH
/Times-Roman SF
22395 XM
(\050June 1990\051.)SH
/Times-Bold SF
9504 16099 MT
(34.)SH
/Times-Roman SF
11604 XM
(R. L. Goodstein.)SH
/Times-Italic SF
20171 XM
(Recursive Number Theory.)SH
/Times-Roman SF
33670 XM
(North-Holland Publishing Company,)SH
9504 17385 MT
(Amsterdam, 1964.)SH
/Times-Bold SF
9504 19494 MT
(35.)SH
/Times-Roman SF
11604 XM
(C. A. R. Hoare. "An Axiomatic Basis for Computer Programming".)SH
/Times-Italic SF
45020 XM
(Comm. ACM)SH
9504 20780 MT
(12)SH
/Times-Roman SF
(, 10 \0501969\051, 576-583.)SH
/Times-Bold SF
9504 22889 MT
(36.)SH
/Times-Roman SF
11604 XM
(L. Hodes. Solving Problems by Formula Manipulation. Proc. Second Inter. Joint)SH
9504 24175 MT
(Conf. on Art. Intell., The British Computer Society, 1971, pp. 553-559.)SH
/Times-Bold SF
9504 26284 MT
(37.)SH
/Times-Roman SF
11604 XM
(C.-H. Huang and C. Lengauer. "The Automated Proof of a Trace Transformation)SH
9504 27570 MT
(for a Bitonic Sort".)SH
/Times-Italic SF
19263 XM
(Theoretical Computer Science 1)SH
/Times-Roman SF
(, 46 \0501986\051, 261-284.)SH
/Times-Bold SF
9504 29679 MT
(38.)SH
/Times-Roman SF
11604 XM
(W. A. Hunt. "Microprocessor Design Verification".)SH
/Times-Italic SF
37318 XM
(Journal of Automated)SH
9504 30965 MT
(Reasoning 5)SH
/Times-Roman SF
(, 4 \0501989\051, 429-460.)SH
/Times-Bold SF
9504 33074 MT
(39.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A Formal Semantics and Proof of Soundness for the Logic of the)SH
9504 34360 MT
(NQTHM Version of the Boyer-Moore Theorem Prover. Internal Note 229, Institute for)SH
9504 35646 MT
(Computing Science, University of Texas at Austin, February, 1987.)SH
/Times-Bold SF
9504 37755 MT
(40.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A Mechanically-checked Semi-interactive Proof of Correctness of)SH
9504 39041 MT
(Gries's Algorithm for Finding the Largest Size of a Square True Submatrix. Internal)SH
9504 40327 MT
(Note 236, Institute for Computing Science, University of Texas at Austin, October,)SH
9504 41613 MT
(1986.)SH
/Times-Bold SF
9504 43722 MT
(41.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. An Example in NQTHM: Ramsey's Theorem. Internal Note 100,)SH
9504 45008 MT
(Computational Logic, Inc., November, 1988.)SH
/Times-Bold SF
9504 47117 MT
(42.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. Boyer-Moore-ish Micro Gypsy and a Prototype Hardware)SH
9504 48403 MT
(Expander. Internal)
300 W( Note 73, Computational Logic, Inc., August, 1988.)SH
/Times-Bold SF
9504 50512 MT
(43.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A Mutual Recursion and Dependency Analysis Tool for NQTHM.)SH
9504 51798 MT
(Internal Note 99, Computational Logic, Inc., 1988.)SH
/Times-Bold SF
9504 53907 MT
(44.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A User's Manual for RCL. Internal Note 157, Computational)SH
9504 55193 MT
(Logic, Inc., October, 1989.)SH
/Times-Bold SF
9504 57302 MT
(45.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann and Matt Wilding. A Parallel Version of the Boyer-Moore Prover.)SH
9504 58588 MT
(Tech. Rept. 39, Computational Logic, Inc., February, 1989.)SH
/Times-Bold SF
9504 60697 MT
(46.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. DEFN-SK: An Extension of the Boyer-Moore Theorem Prover to)SH
9504 61983 MT
(Handle First-Order Quantifiers. Tech. Rept. 43, Computational Logic, Inc., 1717 W. 6th)SH
9504 63269 MT
(St, Suite 290, Austin, Texas, June, 1989.)SH
/Times-Bold SF
9504 65378 MT
(47.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. Addition of Free Variables to an Interactive Enhancement of the)SH
9504 66664 MT
(Boyer-Moore Theorem Prover. Tech. Rept. 42, Computational Logic, Inc., Austin,)SH
9504 67950 MT
(Texas, May, 1989.)SH
ES
%%Page: 16 17
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(16)SH
12 /Times-Bold AF
9504 8023 MT
(48.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A Mechanically-checked Correctness Proof for Generalization in)SH
9504 9309 MT
(the Presence of Free Variables. Tech. Rept. 53, Computational Logic, Inc., Austin,)SH
9504 10595 MT
(Texas, March, 1990.)SH
/Times-Bold SF
9504 12704 MT
(49.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. An Integer Library for NQTHM. Internal Note 182,)SH
9504 13990 MT
(Computational Logic, Inc., March, 1990.)SH
/Times-Bold SF
9504 16099 MT
(50.)SH
/Times-Roman SF
11604 XM
(Leslie Lamport, Robert Shostak, and Marshall Pease. "The Byzantine Generals)SH
9504 17385 MT
(Problem".)SH
/Times-Italic SF
14962 XM
(ACM TOPLAS 4)SH
/Times-Roman SF
(, 3 \050July 1982\051, 382-401.)SH
/Times-Bold SF
9504 19494 MT
(51.)SH
/Times-Roman SF
11604 XM
(C. Lengauer. "On the Role of Automated Theorem Proving in the Compile-Time)SH
9504 20780 MT
(Derivation of Concurrency".)SH
/Times-Italic SF
23827 XM
(Journal of Automated Reasoning 1)SH
/Times-Roman SF
(, 1 \0501985\051, 75-101.)SH
/Times-Bold SF
9504 22889 MT
(52.)SH
/Times-Roman SF
11604 XM
(C. Lengauer and C.-H. Huang. A Mechanically Certified Theorem about Optimal)SH
9504 24175 MT
(Concurrency of Sorting Networks. Proc. 13th Ann. ACM Symp. on Principles of)SH
9504 25461 MT
(Programming Languages, 1986, pp. 307-317.)SH
/Times-Bold SF
9504 27570 MT
(53.)SH
/Times-Roman SF
11604 XM
(D. Loveland.)SH
/Times-Italic SF
18503 XM
(Automated Theorem Proving: A Logical Basis.)SH
/Times-Roman SF
41938 XM
(North Holland,)SH
9504 28856 MT
(Amsterdam, 1978.)SH
/Times-Bold SF
9504 30965 MT
(54.)SH
/Times-Roman SF
11604 XM
(J. McCarthy. "Recursive Functions of Symbolics Expressions and their)SH
9504 32251 MT
(Computation by Machine".)SH
/Times-Italic SF
23163 XM
(Communications of the Association for Computing)SH
9504 33537 MT
(Machinery 3)SH
/Times-Roman SF
(, 4 \0501960\051, 184-195.)SH
/Times-Bold SF
9504 35646 MT
(55.)SH
/Times-Roman SF
11604 XM
(J. McCarthy.)SH
/Times-Italic SF
18438 XM
(The Lisp Programmer's Manual.)SH
/Times-Roman SF
34906 XM
(M.I.T. Computation Center, 1960.)SH
/Times-Bold SF
9504 37755 MT
(56.)SH
/Times-Roman SF
11604 XM
(J. McCarthy. Towards a Mathematical Science of Computation. Proceedings of)SH
9504 39041 MT
(IFIP Congress, 1962, pp. 21-28.)SH
/Times-Bold SF
9504 41150 MT
(57.)SH
/Times-Roman SF
11604 XM
(J. McCarthy. Computer Programs for Checking Mathematical Proofs. Recursive)SH
9504 42436 MT
(Function Theory, Proceedings of a Symposium in Pure Mathematics, Providence, Rhode)SH
9504 43722 MT
(Island, 1962, pp. 219-227.)SH
/Times-Bold SF
9504 45831 MT
(58.)SH
/Times-Roman SF
11604 XM
(J. McCarthy. A Basis for a Mathematical Theory of Computation. In)SH
/Times-Italic SF
45475 XM
(Computer)SH
9504 47117 MT
(Programming and Formal Systems)SH
/Times-Roman SF
(, P. Braffort and D. Hershberg, Eds., North-Holland)SH
9504 48403 MT
(Publishing Company, Amsterdam, The Netherlands, 1963.)SH
/Times-Bold SF
9504 50512 MT
(59.)SH
/Times-Roman SF
11604 XM
(J. McCarthy, et al.)SH
/Times-Italic SF
21072 XM
(LISP 1.5 Programmer's Manual.)SH
/Times-Roman SF
37572 XM
(The MIT Press, Cambridge,)SH
9504 51798 MT
(Massachusetts, 1965.)SH
/Times-Bold SF
9504 53907 MT
(60.)SH
/Times-Roman SF
11604 XM
(J S. Moore. "A Mechanical Proof of the Termination of Takeuchi's Function".)SH
/Times-Italic SF
9504 55193 MT
(Information Processing Letters 9)SH
/Times-Roman SF
(, 4 \0501979\051, 176-181.)SH
/Times-Bold SF
9504 57302 MT
(61.)SH
/Times-Roman SF
11604 XM
(J. S. Moore. "A Mechanically Verified Language Implementation".)SH
/Times-Italic SF
44853 XM
(Journal of)SH
9504 58588 MT
(Automated Reasoning 5)SH
/Times-Roman SF
(, 4 \0501989\051, 461-492.)SH
/Times-Bold SF
9504 60697 MT
(62.)SH
/Times-Roman SF
11604 XM
(J. S. Moore, et. al. "Special Issue on System Verification".)SH
/Times-Italic SF
40589 XM
(Journal of Automated)SH
9504 61983 MT
(Reasoning 5)SH
/Times-Roman SF
(, 4 \0501989\051, 409-530.)SH
/Times-Bold SF
9504 64092 MT
(63.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-)SH
9504 65378 MT
(Moore Theorem Prover. Tech. Rept. 19, Computational Logic, Inc., Austin, Texas,)SH
9504 66664 MT
(May, 1988.)SH
/Times-Bold SF
9504 68773 MT
(64.)SH
/Times-Roman SF
11604 XM
(Marshall Pease, Robert Shostak, and Leslie Lamport. "Reaching Agreement in the)SH
9504 70059 MT
(Presence of Faults".)SH
/Times-Italic SF
19695 XM
(JACM 27)SH
/Times-Roman SF
(, 2 \050April 1980\051, 228-234.)SH
ES
%%Page: 17 18
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(17)SH
12 /Times-Bold AF
9504 8023 MT
(65.)SH
/Times-Roman SF
11604 XM
(J. A. Robinson. "A Machine-oriented Logic Based on the Resolution Principle".)SH
/Times-Italic SF
9504 9309 MT
(JACM 12)SH
/Times-Roman SF
(, 1 \0501965\051, 23-41.)SH
/Times-Bold SF
9504 11418 MT
(66.)SH
/Times-Roman SF
11604 XM
(David M. Russinoff. "An Experiment with the Boyer-Moore Theorem Prover: A)SH
9504 12704 MT
(Proof of Wilson's Theorem".)SH
/Times-Italic SF
24129 XM
(Journal of Automated Reasoning 1)SH
/Times-Roman SF
(, 2 \0501985\051, 121-139.)SH
/Times-Bold SF
9504 14813 MT
(67.)SH
/Times-Roman SF
11604 XM
(N. Shankar. "Towards Mechanical Metamathematics".)SH
/Times-Italic SF
38718 XM
(Journal of Automated)SH
9504 16099 MT
(Reasoning 1)SH
/Times-Roman SF
(, 4 \0501985\051, 407-434.)SH
/Times-Bold SF
9504 18208 MT
(68.)SH
/Times-Roman SF
11604 XM
(N. Shankar. A Mechanical Proof of the Church-Rosser Theorem. Tech. Rept.)SH
9504 19494 MT
(ICSCA-CMP-45, Institute for Computing Science, University of Texas at Austin, 1985.)SH
/Times-Bold SF
9504 21603 MT
(69.)SH
/Times-Roman SF
11604 XM
(N. Shankar.)SH
/Times-Italic SF
17903 XM
(Proof Checking Metamathematics)SH
/Times-Roman SF
(. Ph.D.)
300 W( Th., University of Texas at)SH
9504 22889 MT
(Austin, 1986.)SH
/Times-Bold SF
9504 24998 MT
(70.)SH
/Times-Roman SF
11604 XM
(J. R. Shoenfield.)SH
/Times-Italic SF
20172 XM
(Mathematical Logic.)SH
/Times-Roman SF
30774 XM
(Addison-Wesley, Reading, Ma., 1967.)SH
/Times-Bold SF
9504 27107 MT
(71.)SH
/Times-Roman SF
11604 XM
(T. Skolem. The Foundations of Elementary Arithmetic Established by Means of the)SH
9504 28393 MT
(Recursive Mode of Thought, without the Use of Apparent Variables Ranging over)SH
9504 29679 MT
(Infinite Domains. In)SH
/Times-Italic SF
19873 XM
(From Frege to Godel)SH
/Times-Roman SF
(, J. van Heijenoort, Ed., Harvard University)SH
9504 30965 MT
(Press, Cambridge, Massachusetts, 1967.)SH
/Times-Bold SF
9504 33074 MT
(72.)SH
/Times-Roman SF
11604 XM
(G. L. Steele, Jr.)SH
/Times-Italic SF
19704 XM
(Common Lisp The Language.)SH
/Times-Roman SF
34504 XM
(Digital Press, 30 North Avenue,)SH
9504 34360 MT
(Burlington, MA 01803, 1984.)SH
/Times-Bold SF
9504 36469 MT
(73.)SH
/Times-Roman SF
11604 XM
(J. von Neumann.)SH
/Times-Italic SF
20337 XM
(John von Neumann, Collected Works, Volume V.)SH
/Times-Roman SF
44369 XM
(Pergamon)SH
9504 37755 MT
(Press, Oxford, 1961.)SH
/Times-Bold SF
9504 39864 MT
(74.)SH
/Times-Roman SF
11604 XM
(L. Wos, et al. "The concept of demodulation in theorem proving".)SH
/Times-Italic SF
44154 XM
(Journal of the)SH
9504 41150 MT
(ACM 14)SH
/Times-Roman SF
13837 XM
(\0501967\051, 698-709.)SH
/Times-Bold SF
9504 43259 MT
(75.)SH
/Times-Roman SF
11604 XM
(Matt Kaufmann and William D. Young. Comparing Gypsy and the Boyer-Moore)SH
9504 44545 MT
(Logic for Specifying Secure Systems. Institute for Computing Science, University of)SH
9504 45831 MT
(Texas at Austin, May, 1987. ICSCA-CMP-59.)SH
/Times-Bold SF
9504 47940 MT
(76.)SH
/Times-Roman SF
11604 XM
(W. D. Young. "A Mechanically Verified Code Generator".)SH
/Times-Italic SF
40781 XM
(Journal of Automated)SH
9504 49226 MT
(Reasoning 5)SH
/Times-Roman SF
(, 4 \0501989\051, 493-518.)SH
/Times-Bold SF
9504 51335 MT
(77.)SH
/Times-Roman SF
11604 XM
(Yuan Yu. "Computer Proofs in Group Theory".)SH
/Times-Italic SF
35350 XM
(Journal of Automated Reasoning)SH
/Times-Roman SF
9504 52621 MT
(\0501990\051. To appear.)SH
ES
%%Page: i 19
BS
0 SI
15 /Times-Bold AF
25517 12220 MT
(Table of Contents)SH
13 /Times-Roman AF
12104 16712 MT
(1. Introduction)
SH( .)
74 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(2)SH
12104 18089 MT
(2. The Logic)
SH( .)
472 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(2)SH
12104 19466 MT
(3. The Prover)
SH( .)
38 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(3)SH
12 SS
13104 20752 MT
(3.1. How to Get a Copy)
SH( .)
568 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(3)SH
13104 22038 MT
(3.2. WARNING: Difficulty of Use)
SH( .)
368 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(4)SH
13104 23324 MT
(3.3. Heuristic Character of NQTHM)
SH( .)
535 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(4)SH
13104 24610 MT
(3.4. Induction)
SH( .)
499 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(4)SH
13104 25896 MT
(3.5. Simplification)
SH( .)
29 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(5)SH
13104 27182 MT
(3.6. Other Heuristics)
SH( .)
199 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(5)SH
13 SS
12104 28559 MT
(4. The Importance of the User in Finding Proofs)
SH( .)
258 W( . . . . . . . . . . . . . . . .)SH
51550 XM
(5)SH
12104 29936 MT
(5. Our Motivation: Computer System Correctness)
SH( .)
401 W( . . . . . . . . . . . . . .)SH
51550 XM
(6)SH
12104 31313 MT
(6. Applications)
SH( .)
507 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(6)SH
12104 32690 MT
(7. Work in Progress: ACL2)
SH( .)
290 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(7)SH
12104 34067 MT
(8. Conclusions)
SH( .)
72 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51550 XM
(9)SH
12 SS
13104 35353 MT
(8.1. Proof Checking as a Mere Engineering Challenge)
SH( .)
433 W( . . . . . . . . . . . . . . .)SH
51600 XM
(9)SH
13104 36639 MT
(8.2. Checking the Correctness of Computing Systems)
SH( .)
62 W( . . . . . . . . . . . . . . . .)SH
51600 XM
(9)SH
13104 37925 MT
(8.3. Formalizing the Real World)
SH( .)
597 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51000 XM
(10)SH
13 SS
12104 39302 MT
(9. Acknowledgements)
SH( .)
75 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
50900 XM
(10)SH
10 SS
30713 75600 MT
(i)SH
ES
%%Trailer
%%Pages: 19
%%DocumentFonts: Times-Roman Times-Bold Times-Italic Courier-Bold Symbol