Elimination of Negation in a Logical Framework

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.