Alberto Momigliano (Leicester)

Logical frameworks with a logic programming interpretation such as

hereditary Harrop formulae (HHF) (Miller et al. 1991) 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 (1984) for Horn logic to a fragment of higher-order HHF. This

entails finding a middle ground between the Closed World Assumption

usually associated with negation and the Open World Assumption

typical of logical frameworks; the main technical ideas are to isolate

a set of programs where static and dynamic clauses do not overlap and
to

formulate a (strict) relevant lambda-calculus which is closed under
term

complementation.