Since the advent of Horn-clause logic programming in the mid 1970's, there have been numerous attempts to extend the expressive power of Horn-clause logic while preserving some of its attractive computational properties. This article, the first of a pair, presents a clausal language that extends Horn-clause logic by adding negations and embedded implications to the righthand side of a rule, and interpreting these new rules intuitionistically, in a set of partial models. The resulting system is shown to have a fixed-point semantics that generalizes the van Emden-Kowalski semantics for Horn clauses. © 1988.
McCarty, L. T. (1988). Clausal intuitionistic logic I. fixed-point semantics. The Journal of Logic Programming, 5(1), 1–31. https://doi.org/10.1016/0743-1066(88)90005-2