Minimal negation and Hereditary Harrop formulae

Following an underrated paper by Miller [7], minimal negation is added to first-order Hereditary Harrop-formulae (fohh) at no computational cost, preserving their nature of abstract logic programming language [8]. The soundness and completeness theorem is proved with respect to natural deduction. The following relation with negation-as-failure holds: G has a SLDNF derivation from P iff G has a uniform proof from the completion of P. Moreover we show how to embed minimal, intuitionistic and classical logic into fohh: as a consequence and application of the two last results, the logic is shown to represent every partial recursive functions.