A COMPUTER SYSTEM FOR CHECKING PROOFS
Original Publication Date: 1981-Jan-31
Included in the Prior Art Database: 2007-Mar-29
Software Patent Institute
Johnson, Scott D.: AUTHOR [+2]
A CO!QUTER SYSTEM FOR C:HECKING PROOFS Scott D. Johnson Ph.D. Thesis January 1981
A CO!QUTER SYSTEM FOR C:HECKING PROOFS Scott D. Johnson
Department of Conputer Science
Ithaca, Hew York, 1L853
A COMPUTER SYSTi3 FOR CHECKING PROOFS
Presented to the Faculty of the Creduete Scb.ccl of Cornell C'niversity
in PsrtiaL Fulfillment for the Degree of Coctor of Philosophy
Scott David Johnson was born on October 16s 1953 in Joliet. Illinois. He gradunted from Joliet Township High School. West Campus. in 1971. Ee received the Bachelor of Science degree in computer science from the Illi- nois Institute of Technology in 1375. greduating vith high honors. In 1579 he received the degree of Kaster of Science in ccnputer science Erorc Cor- nell University. During the 1939-80 academic year. he vas an instroctor
at Cornell University. He has accepted a position with the the Wcscerr. Development Laboratories of the Ford Aerospace Corporation.
Scott David Johnson Jsnunry 1301
wnnt to thnnk the Academy. my family, Hnrry w!to feA my do8
..." I once tkought the loq-vinded speecheĉhose pco- pie gLve vere rather contrived. But faced with the task of writing this eectlonr I think I know just how they fee:.
First of all. I must thank m$ ndvibor Bob Constable. If it were not fur n l i thc! cnrrotn'nad nticka (suatiy cnrruta) Ira lrna c~acd on n~c ovcr Lira past few yearc, this thesis would bnve never been completed. Bob has a vonderful senfie of optimism. and together we have embarked on projects I would have never attempted on my ovn.
I am also deeply grateful to Denn Krafft and Dan Zlatin. The algo- ritl~mb I prov~.d I n Chul,lcrs 5 . 6, rind 7 wcris dcv~lopcd in collaboratio~l
vi:h Dean and Dan, each of whom worked on the implementation of the V-code Interpreter. They carefully read drafts cf the thesis and found countless errors. I wont to enpecinlly tl.n:ik Dean for performing the llcrculenn tnok of wading thror~gh an exceedingly rough draft of Chapter 6.
I would also like to mention the other people who have worked on the ?L/CV project. Mike O'Donnell was the principle designer of PL/CVl, and gnve helpful advice during the design of PLICVZ. Carl Hnuser helped write the manual for PL/CV1. Mike O'Donnell and Tat-Hung Chan developed the arithmetic package used in PL/CVZ; Carl Cichenlaub later added some exten- siocs this 2ackage. Ryan Stansifer is currently translating the nrith- metic package and V-code Interpreter into the C programming language so tbat it can be used by AVID, an interactive version of PL/CV being developed by Dean Krafft.
While I was'warking on the PL/CV project I was supported by the
I.'ri:ionr~I Fcirlrco Fc,\rilJution. Cr...