Extensional Higher-Order Logic Programming

TL;DR

This paper introduces a purely extensional semantics for higher-order logic programming, establishing a theoretical framework that generalizes classical logic programming with a sound and complete proof procedure.

Contribution

It develops a novel extensional semantics for higher-order logic programming and provides a sound and complete SLD-resolution proof method.

Findings

Unique minimum Herbrand model for each program

Semantics based on set equality of predicates

Sound and complete proof procedure

Abstract

We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique minimum Herbrand model which is the greatest lower bound of all Herbrand models of the program and the least fixed-point of an immediate consequence operator. We also propose an SLD-resolution proof procedure which is proven sound and complete with respect to the minimum model semantics. In other words, we provide a purely extensional theoretical framework for higher-order logic programming which generalizes the familiar theory of classical (first-order) logic programming.