Affordable Access

Publisher Website

A Structure-preserving Clause Form Translation

Authors
Journal
Journal of Symbolic Computation
0747-7171
Publisher
Elsevier
Publication Date
Volume
2
Issue
3
Identifiers
DOI: 10.1016/s0747-7171(86)80028-1
Disciplines
  • Logic
  • Mathematics

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

On Different Structure-preserving Translations to...

on Journal of Symbolic Computatio... Jan 01, 1996

An optimality result for clause form translation

on Journal of Symbolic Computatio... Jan 01, 1992

Formal methodology of translation. I. Semantic pre...

on Information and Control Jan 01, 1978
More articles like this..