A Proof Procedure Using Connection Graphs
Citations Over TimeTop 1% of 1975 papers
Abstract
Various deficiencies of resolution systems are investigated and a new theorem-proving system designed to remedy those deficiencms is presented The system is notable for eliminating redundancies present in SL-resolutlon, for incorporating preprocessing procedures, for liberahzing the order in which subgoals can be activated, for incorporating multidirectmnal searches, and for giving immediate access to pairs of clauses which resolve Examples of how the new system copes with the defic2encies of other theorem-proving systems are chosen from the areas of predicate logic programming and language parsing. The paper emphasizes the historical development of the new system, beginning as a supplement to SL-resolution in the form of classificatmn trees and incorporating an analogue of the Waltz algorithm for picture Interpretation The paper ends with a discussion of the opportunities for using look-ahead to guide the search for proofs
Related Papers
- → THE CONJUGATE CONNECTION OF A YANG-MILLS CONNECTION(2008)7 cited
- → A Study on Layer Connection Strategies in Stacked Convolutional Deep Belief Networks(2014)1 cited
- → On Generalized h-Recurrent Finsler Connection(2021)
- → Book Review: The Puritan in England and New England(1990)
- On the Finsler Connection Associated with a Linear Connection Satisfying P^h_ =0(1978)