Show simple item record

dc.contributor.advisorMeltzer, Bernarden
dc.contributor.authorKowalski, Robert Anthonyen
dc.date.accessioned2013-04-19T12:27:03Z
dc.date.available2013-04-19T12:27:03Z
dc.date.issued1970
dc.identifier.urihttp://hdl.handle.net/1842/6674
dc.description.abstractInference systems Τ and search strategies E for T are distinguished from proof procedures β = (T,E) The completeness of procedures is studied by studying separately the completeness of inference systems and of search strategies. Completeness proofs for resolution systems are obtained by the construction of semantic trees. These systems include minimal α-restricted binary resolution, minimal α-restricted M-clash resolution and maximal pseudo-clash resolution. Certain refinements of hyper-resolution systems with equality axioms are shown to be complete and equivalent to refinements of the pararmodulation method for dealing with equality. The completeness and efficiency of search strategies for theorem-proving problems is studied in sufficient generality to include the case of search strategies for path-search problems in graphs. The notion of theorem-proving problem is defined abstractly so as to be dual to that of and" or tree. Special attention is given to resolution problems and to search strategies which generate simpler before more complex proofs. For efficiency, a proof procedure (T,E) requires an efficient search strategy E as well as an inference system T which admits both simple proofs and relatively few redundant and irrelevant derivations. The theory of efficient proof procedures outlined here is applied to proving the increased efficiency of the usual method for deleting tautologies and subsumed clauses. Counter-examples are exhibited for both the completeness and efficiency of alternative methods for deleting subsumed clauses. The efficiency of resolution procedures is improved by replacing the single operation of resolving a clash by the two operations of generating factors of clauses and of resolving a clash of factors. Several factoring methods are investigated for completeness. Of these the m-factoring method is shown to be always more efficient than the Wos-Robinson method.en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionHayes, P.J. and Kowalski, R.A., Semantic trees in in automatic theorem-proving, Machine Intelligence 4. Edinburgh University Press (1969) pp. 87-101.en
dc.relation.hasversionKowalski, R,L., Panel discussion, 11ormal systems and non-numerical problem solving by computers. Fcurth Systems Symposium, Case Western Reserve University, Cleveland, Ohio (November 1968).en
dc.relation.hasversionKowalski, R.A., Search strategies for theorem-proving. Machine Intelligence 5, Edinburgh University Press (1970) pp. 181-201.en
dc.subjectInference systemsen
dc.subjectsearch strategiesen
dc.subjectAutomatic theorem provingen
dc.subjectProof theoryen
dc.titleStudies in the completeness and efficiency of theorem-proving by resolutionen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record