Alberto Momigliano

Elimination of Negation in a Logical Framework

Logical frameworks with a logic programming interpretation such as
hereditary Harrop formulae (HHF) \cite{Miller91apal} 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 \emph{elimination} of
negation introduced in \cite{Sato84} 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, that we call the Regular
World Assumption; the main technical idea is to isolate a set of
programs where static and dynamic clauses do not overlap.