The problem of translating a formula into a “good” clause form is known to be a very important one in resolution automated theorem proving. Some theorems have such a huge clause form that it is practically impossible to prove them by resolution. Several methods exist to reduce clause forms, some applied before and some after translation. They are generally based on (local or non-local) simplifications. A method consisting in the creation and use of definitions, which we call renaming, has been developed in [5], [4] and [7]. Applying it in an exhaustive way was shown to yield a translation into clause form polynomial in size (see [7]). In this paper we investigate non exhaustive renamings in the purpose of minimizing the number of clauses. We obtain a translation which is shown to be polynomial in size, and optimal in number of clauses when the theorem contains no equivalence. An example shows that this translation is not necessarily optimal in presence of equivalence. Experiments with “challenge” examples show the practical efficiency of this translation.
CITATION STYLE
de la Tour, T. B. (1990). Minimizing the number of clauses by renaming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 449 LNAI, pp. 558–572). Springer Verlag. https://doi.org/10.1007/3-540-52885-7_114
Mendeley helps you to discover research relevant for your work.