A transformational approach to constructive negation in constraint normal logic programming

Resumo

In this dissertation, we propose an efficient treatment of constructive negation in constraint normal logic programming by means of a sound and complete procedural semantics, which is not based on subsidiary computation trees, Additionally, we provide solutions to other main problems related with negation: general equality constraint solving and local variable elimination via program transformation. Concerning equality constraint solving, we present a new notion of normal form that, in combination with the classical quantifier elimination technique, allows to eliminate the whole prefix of quantifiers from any prenex formula in an efficient way. Our method takes advantage of two main features of our normal form, which are a compact representation of solutions and an efficient satisfiability test. Regarding the elimination of local variables, which are the unique source of inefficiency in our treatment of constructive negation, we study the transformation of normal logic programs involving negation. Specifically, we focus on unfold/fold based transformation systems and, in particular, in the folding rule, proposing a new unfold/fold mechanism that extends the ones in the literature. With the help of the proposed transformation system, we also provide an algorithm that successfully eliminates local variables from normal logic programs.