On Matrices with Connections
- 1 October 1981
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 28 (4), 633-645
- https://doi.org/10.1145/322276.322277
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 wayKeywords
This publication has 17 references indexed in Scilit:
- A theoretical basis for the systematic proof methodPublished by Springer Nature ,2005
- Theorem Proving via General MatingsJournal of the ACM, 1981
- Tautology testing with a generalized matrix reduction methodTheoretical Computer Science, 1979
- Non-resolution theorem provingArtificial Intelligence, 1977
- Towards feasible solutions of the tautology problemAnnals of Mathematical Logic, 1976
- Refutation graphsArtificial Intelligence, 1976
- On Algorithms for Enumerating All Circuits of a GraphSIAM Journal on Computing, 1976
- A Proof Procedure Using Connection GraphsJournal of the ACM, 1975
- A proof procedure with matrix reductionPublished by Springer Nature ,1970
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965