On Matrices with Connections

Abstract

Theorem proving is considered as the problem of verifying that each path through a matrix consisting of a set of clauses can be made complementary. By introducing connections to such a matrix the followmg three results are derived from that conceptual basis. First, a sunple and short proof for the consistency and completeness of the connection graph procedure as given Second, a macrosimplificatlon rule for the preparatory step of any ATP-method is defined which, like the deletion or subsumptlon rules, properly reduces a given matrix whenever it apphes It can be regarded as a generalization to arbitrary clauses of the well-known fact that sets of two-lateral clauses can be decided quickly Finally, m view of the relation between resolution-based and natural-deduction-based methods, a constructive transformation is specified which explicitly relates each resolution step to a pair of complementary literals in an axiom of a natural deduction, and wce versa. Although the treatment is restricted to the ground case, it is obvious that all results can be easily lifted to the general case in the usual way. © 1981, ACM. All rights reserved.