A structure-preserving clause form translation. (English) Zbl 0636.68119
Summary: Most resolution theorem provers convert a theorem into clause form before attempting to find a proof. The conventional translation of a first-order formula into clause form often obscures the structure of the formula, and may increase the length of the formula by an exponential amount in the worst case. We present a non-standard clause form translation that preserves more of the structure of the formula than the conventional translation. This new translation also avoids the exponential increase in size which may occur with the standard translation.
We show how this idea may be combined with the idea of replacing predicates by their definitions before converting to clause form. We give a method of lock resolution which is appropriate for the non-standard clause form translation, and which has yielded a spectacular reduction in search space and time for one example. These techniques should increase the attractiveness of resolution theorem provers for program verification applications, since the theorems that arise in program verification are often simple but tedious for humans to prove.
We show how this idea may be combined with the idea of replacing predicates by their definitions before converting to clause form. We give a method of lock resolution which is appropriate for the non-standard clause form translation, and which has yielded a spectacular reduction in search space and time for one example. These techniques should increase the attractiveness of resolution theorem provers for program verification applications, since the theorems that arise in program verification are often simple but tedious for humans to prove.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Bledsoe, W., Splitting and reduction heuristics in automatic theorem proving, Artif. Intell., 2, 55-77 (1971) · Zbl 0221.68052 |
| [2] | Bledsoe, W., The UT natural deduction prover, (University of Texas Mathematics Dept. Memo ATP-1713 (1983)) |
| [3] | Bledsoe, W., Some automatic proofs in analysis, (Bledsoe, W.; Loveland, D., Automated Theorem Proving: After 25 Years. Automated Theorem Proving: After 25 Years, Contemporary Mathematics, 29 (1984), American Mathematical Society: American Mathematical Society New York), 89-118 · Zbl 0585.68079 |
| [4] | Boyer, R., Locking, a Restriction of Resolution, (Ph.D. thesis, University of Texas at Austin (1971)) |
| [5] | Chang, C.; Lee, R., (Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press New York) · Zbl 0263.68046 |
| [6] | Charniak, E.; Riesbeck, C.; McDermott, D., (Artificial Intelligence Programming (1980), Erlbaum Associates: Erlbaum Associates New Jersey) · Zbl 0518.68055 |
| [7] | Eder, E., An implementation of a theorem prover based on the connection method, (Bibel, W.; Petkoff, B., AIMSA ’84, Artificial Intelligence—Methodology Systems Applications, Varna, Bulgaria, September 1984 (1984), North-Holland: North-Holland Amsterdam), 121-128 |
| [8] | Greenbaum, S.; Nagasaka, P.; O’Rorke, P.; Plaisted, D., Comparison of natural deduction and locking resolution implementations, (Loveland, D., Proceedings of 6th Conference on Automated Deduction. Proceedings of 6th Conference on Automated Deduction, Springer Lec. Notes Comp. Sci., 138 (1982)), 159-171 |
| [9] | Lame, D., (Personal communication (1984)) |
| [10] | Loveland, D., (Automated Theorem Proving: A Logical Basis (1978), North-Holland: North-Holland New York) · Zbl 0364.68082 |
| [11] | Murray, N., Completely non-clausal theorem proving, Artif. Intell., 18, 67-85 (1982) · Zbl 0472.68053 |
| [12] | Nelson, G.; Oppen, D., Simplification by cooperating decision procedures, ACM Trans. Prog. Lang, Syst., 1, 245-257 (1979) · Zbl 0452.68013 |
| [13] | Nelson, G.; Oppen, D., Fast decision procedures based on congruence closure, J. Assoc. Comp. Mach., 27, 356-364 (1980) · Zbl 0441.68111 |
| [14] | Shostak, R., On the SUP-INF method for proving Presburger formulas, J. Assoc. Comp, Mach., 24, 529-543 (1977) · Zbl 0423.68052 |
| [15] | Tseitin, G., On the complexity of derivations in propositional calculus, (Siekmann, J.; Wrightson, G., Automation of Reasoning 2: Classical Papers on Computational Logic (1983), SpringerVerlag: SpringerVerlag Berlin), 466-483 |
| [16] | Wos, L.; Robinson, G.; Carson, D.; Shalla, L., The concept of demodulation in theorem proving, J. Assoc. Comp. Mach., 14, 698-709 (1967) · Zbl 0157.02501 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
