×

Clausal intuitionistic logic. I: Fixed-point semantics. (English) Zbl 0645.03006

The aim of this paper is the extension of Horn clause logic in order to get a more expressive language without sacrificing the efficiency of computational interpretations. The extension consists in the introduction of 2 new types of rules: 1) a negation rule of the form P(x)\(\leftarrow \neg Q(x,y)\) and 2) an embedded implication rule of the form P(x)\(\leftarrow [Q(x,y)\to R(x,y)]\). The author defines an intuitionistic semantics for the classical Horn rules and for the new rules as well. W.r.t. fixed point semantics, it turns out that the greatest fixed point of the transformations is of major interest (compared with the least fixed point for classical Horn logic [M. H. van Emden and R. A. Kowalski, J. Assoc. Comput. Mach. 23, 733-742 (1976; Zbl 0339.68004)]. However, the fixed point theorem is somewhat weaker, because the iterations of the operators have to be extended beyond \(\omega\). On the other hand, it is shown, that the model intersection property holds for the new interpretation concept as well. An extension of Horn clause reflutation trees to a structure for the extended languages and thus a completeness result w.r.t. the new semantics is left to part II of this paper.
Reviewer: A.Leitsch

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations

Citations:

Zbl 0339.68004
Full Text: DOI