Some contributions to the semantics of normal logic programs

Zusammenfassung

In this dissertation we study different problems that arise when providing semantics to normal logic programs, On one hand, since constructive negation can be naturally formulated in terms of constraint logic programming, we deal with the class of constraint normal logic programs. Indeed, we propose a new operational semantics for normal logic programs, called BCN (Basic Constructive Negation), considering constraints over the domain of terms. This operational semantics does not need to deal with subsidiary trees and, for our purposes, is simpler than other existing proposals that use constructive negation. Moreover, from our point of view, the semantics of constraint normal logic programming is not properly defined. In this regard, we present a functorial framework to deal with the semantics of constraint normal logic programs in a novel way. In particular, our approach is based on a reformulation of the notion of constraint domain and, on considering that the semantics of a constraint logic program is a functor parametrized by the constraint domain. In addition, we extend the operational semantics BCN to BCN(X), being X a general constraint domain. On the other hand, we provide semantics for normal logic programs enriched with structuring mechanisms and scoping rules. Specifically, we consider constructive negation and the extension that consists in having expressions of the form Q G in goals, where Q is a program unit, G is a goal and stands for the so-called embedded implication. These expressions can be seen as blocks of programs where Q is used for proving the goal G. In particular, we consider both static and dynamic visibility rules. Therefore, we actually deal with a dynamic class and a static class of normal logic programs. When considering structured normal logic programming, providing semantics to program units is, in general, a difficult task due to the non-monotonic nature of negation. In particular, non-monotonicity makes difficult to show compositionality of the program units and constructions. However, we do not want to impose any kind of syntactic restriction (e.g. stratification) that simplify most constructions and proofs at the cost of strongly limiting generality. In order to overcome problems we provide new semantics definitions for the class of dynamic normal logic programs as well as for the class of static normal logic programs. More precisely, for the dynamic language we follow the classical approach: we first propose an operational semantics. Then, we define a model-theoretic semantics in terms of a sort of ordered structures which are an adaptation of the intuitionistic Beth structures. Finally, an (effective) fix-point semantics is provided and we prove the equivalence between those three semantics. In order to deal with the static language, we first define an operational semantics and then we present an alternative semantics in terms of a transformation of the given structured program into a flat one. We finish by showing that this transformation preserves the computed answers of the given static program.