Browse Prior Art Database

A COMPUTER SYSTEM FOR CHECKING PROOFS

IP.com Disclosure Number: IPCOM000148292D
Original Publication Date: 1981-Jan-31
Included in the Prior Art Database: 2007-Mar-29

Publishing Venue

Software Patent Institute

Related People

Johnson, Scott D.: AUTHOR [+2]

Abstract

A CO!QUTER SYSTEM FOR C:HECKING PROOFS Scott D. Johnson Ph.D. Thesis January 1981

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 2% of the total text.

Page 1 of 174

A CO!QUTER SYSTEM FOR C:HECKING PROOFS Scott D. Johnson

Ph.D. Thesis
January 1981

Department of Conputer Science
Cornell Vniversity
Ithaca, Hew York, 1L853

[This page contains 1 picture or other non-text object]

Page 2 of 174

[This page contains 1 picture or other non-text object]

Page 3 of 174

A COMPUTER SYSTi3 FOR CHECKING PROOFS

               A Thesis
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.

by

Scott David Johnson Jsnunry 1301

[This page contains 1 picture or other non-text object]

Page 4 of 174

wnnt to thnnk the Academy. my family, Hnrry w!to feA my do8

during rebearsa?~

     ..." 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...