This dissertation is concerned with theorem-proving by computer. It does not contain a great number of new results, in the sense of new computational devices for improving the efficiency of theorem-proving programs. Rather it is intended as an account of a new approach to the fundamentals of the subject. It is a work, in the main, of consolidation and entrenchment rather than of extension. Accordingly, rather a large fraction of the total is devoted to an examination - a re-examination in fact, since there have been others before me - of the ideas and presuppositions underlying theorem-proving, and an attempt to uncover the underlying reasons why certain ideas - notably that of search - have arisen so consistently in the history of the -" subject.
Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:586181 |
Date | January 1973 |
Creators | Hayes, Patrick J. |
Contributors | Meltzer, Bernard |
Publisher | University of Edinburgh |
Source Sets | Ethos UK |
Detected Language | English |
Type | Electronic Thesis or Dissertation |
Source | http://hdl.handle.net/1842/8115 |
Page generated in 0.0023 seconds