Extensional Semantics for Higher-Order Logic Programs with Negation

We develop an extensional semantics for higher-order logic programs withnegation, generalizing the technique that was introduced in [Bezem99,Bezem01]for positive higher-order programs. In this way we provide an alternativeextensional semantics for higher-order logic programs with negation to the oneproposed in [CharalambidisER14]. As an immediate useful consequence of ourdevelopments, we define for the language we consider the notions ofstratification and local stratification, which generalize the familiar suchnotions from classical logic programming. We demonstrate that for stratifiedand locally stratified higher-order logic programs, the proposed semanticsnever assigns the unknown truth value. We conclude the paper by providing anegative result: we demonstrate that the well-known stable model semantics ofclassical logic programming, if extended according to the technique of[Bezem99,Bezem01] to higher-order logic programs, does not in general lead toextensional stable models.Comment: 24 pages. Submitted to Logical Methods in Computer Scienc