zbMATH — the first resource for mathematics

An optimality result for clause form translation. (English) Zbl 0772.68079
Summary: The exponential complexity insize of the standard clause form translation is often considered as a serious drawback of the resolution method. Fortunately, a polynomial translation is possible by first introducing definitions, one for each subformula of the conjecture. This exhaustiveness can however be proved inefficient when the length of proofs is considered. In order to improve this interesting technique, we first generalize it to renamings, which consist in introducing definitions only for a subset of subformulas, resulting in a wide set of possible clause forms from a single conjecture. We show how a simple and efficient algorithm yields a renaming which, on equivalence-free conjectures, minimizes the number of clauses among these clause forms. This translation has been tested on the famous challenge problem by P. Andrews, yielding a spectacular reduction in search space and time, and therefore is one of the more simple and general technique to efficiently produce a resolution proof for this problem.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Boy de la Tour, T., Minimizing the number of clauses by renaming, (), 558-572
[2] Boy de la Tour, T., Optimisations par renommage dans la méthode de résolution, ()
[3] Boy de la Tour, T.; Caferra, R.; Chaminade, G., Some tools for an inference laboratory (atinf), (), 744-745
[4] Boy de la Tour, T.; Chaminade, G., The use of renaming to improve the efficiency of clausal theorem proving, ()
[5] Bruschi, M., The halting problem, AAR newsletter, 16, 7-12, (1991)
[6] Guha, A.; Zhang, H., Andrew’s challenge problem: clause conversion and solutions, AAR newsletter, 14, 5-8, (1989)
[7] Henschen, L.; Lusk, E.; Overbeek, R.; Smith, B.; Veroff, R.; Winker, S.; Wos, L., Challenge problem 1, SIGART newsletter, 30-31, (1980)
[8] Pelletier, J., Seventy-five problems for testing automatic theorem provers, Journal of automated reasoning, 2, 191-216, (1986) · Zbl 0642.68147
[9] Plaisted, D.A.; Greenbaum, S., A structure-preserving clause from translation, Journal of symbolic computation, 2, 293-304, (1986) · Zbl 0636.68119
[10] Quaife, A., Andrew’s challenge problem revisited, AAR newsletter, 15, 3-7, (1990)
[11] Tseitin, G.S., On the complexity of derivation in propositional calculus, () · Zbl 0267.02023
[12] Van Gelder, A., A satisfiability tester for non-clausal propositional calculus, (), 101-112 · Zbl 0546.68074
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.