Formalizing Two Fixed Point Semantics for HH(C)

摘要

The scheme HH(C) emerged as a double extension of traditional Logic Programming.On one hand, extending Horn logic to hereditary Harrop formulas (HH), in order toimprove the expressive power; on the other, incorporating constraints, in order to increasethe efficiency.The behavior of such extended CLP programs was explained by means of a sequent calculus that, from every program and set of constraints, exclusivelygenerates uniform proofs - i. e. goal-oriented proofs - for any goal, as well as by means of a goal solving procedure. Hence HH(C) was provided for an operational semantics.Recently, some attempts todefine more declarative semantics for HH(C) have been done by the authors. Here such works are enlarged and improved. Two declarative semantics for HH(C) based on fixed point techniques are revisited. They are proved to be equivalent and the corresponding theorems of soundness and completeness, that relate the sequent calculus (and so the operational semantics) with these semantics, are stated and formally proved. Non trivial proofs are included in the current paper, and every technical aspect is developed.