A structure-preserving clause form translation.

*(English)*Zbl 0636.68119Summary: 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.) |

PDF
BibTeX
XML
Cite

\textit{D. A. Plaisted} and \textit{S. Greenbaum}, J. Symb. Comput. 2, 293--304 (1986; Zbl 0636.68119)

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.