×

zbMATH — the first resource for mathematics

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.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
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, ()
[3] Bledsoe, W., Some automatic proofs in analysis, (), 89-118 · Zbl 0585.68079
[4] Boyer, R., Locking, a restriction of resolution, ()
[5] Chang, C.; Lee, R., ()
[6] Charniak, E.; Riesbeck, C.; McDermott, D., ()
[7] Eder, E., An implementation of a theorem prover based on the connection method, (), 121-128
[8] Greenbaum, S.; Nagasaka, P.; O’Rorke, P.; Plaisted, D., Comparison of natural deduction and locking resolution implementations, (), 159-171
[9] Lame, D., ()
[10] Loveland, D., ()
[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, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.