Subproblem finder and instance checker, two cooperating modules for theorem provers
- 10 August 1986
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 33 (4) , 633-657
- https://doi.org/10.1145/6490.6491
Abstract
Properties are proved about INSTANCE, a theorem prover module that recognizes that a formula is a special case and/or an alphabetic variant of another formula, and about INSURER, another theorem prover module that decomposes a problem, represented by a formula, into independent subproblems, using a conjunction. The main result of INSTANCE is soundness; the main result of INSURER is a maximum decomposition into subproblems (with some provisos). Experimental results show that a connection graph theorem prover extended with these modules is more effective than the resolution-based connection graph theorem prover alone.Keywords
This publication has 3 references indexed in Scilit:
- A paradigm for reasoning by analogyArtificial Intelligence, 1971
- The utility of independent subgoals in theorem provingInformation and Control, 1971
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965