ON DEFINITIONAL TRANSFORMATIONS TO NORMAL FORM FOR INTUITIONISTIC LOGIC

Article type: Research Article

Authors: Egly, Uwe

Affiliations: Abt. Wissensbasierte Systeme 184/3, TU Wien, Treitlstraße 3, A-1040 Wien, e-mail: [email protected]

Abstract: In this paper, we examine different definitional transformations into normal form for intuitionistic logic. In contrast to the classical case, “intuitionistic clauses” may contain implications and quantifiers. Usually, such definitional transformations introduce labels defining subfor-mulae. An obvious optimization is the use of implications instead of equivalences whenever possible, which can reduce the size of the resulting normal form. We compare the optimized transformation with the unoptimized transformation with respect to the shortest cut-free LJ-derivation of the resulting normal forms. The comparison is based on a sequence (Hk)k∈N of formulae for which the following hold: (i) there exist cut-free LJ-proofs of the unoptimized normal form of Hk with length double-exponential in k, and (ii) any cut-free LJ-proof of the optimized normal form of Hk has length non-elementary in k. The reason for the different behaviour is the simulation of analytic cuts by the unoptimized translation, which is not possible when the optimization is applied.

DOI: 10.3233/FI-1997-291208

Journal: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 165-201, 1997