We propose a purely extensional semantics for higher-order logic programming. Under this semantics, every program has a unique minimum Herbrand model which is the greatest lower bound of all Her-brand models of the program and the least fixed-point of the immediate consequence operator of the program. We also propose an SLD-resolution proof procedure which is 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.
展开▼
