Logical frameworks with a logic programming interpretation as hereditary Harrop
formulae cannot express directly negative
information, although negation is a useful specification tool.
Since negation-as-failure does not fit well in a logical framework, especially one
endowed with hypothetical and parametric judgments, we adapt the
idea of elimination of negation introduced by Sato & Tamaki
for Horn logic to a fragment of higher-order HHF. This entails
finding a middle ground between the Closed World Assumption required
by negation and the Open World Assumption typical of logical frameworks; the main
technical idea is to isolate a set of programs where static and
dynamic clauses do not overlap.
