We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint Theory (AFT), a powerful formalism that has successfully been used to give meaning to diverse non-monotonic formalisms. The proposed semantics generalizes the classical two-valued stable model semantics of (Gelfond and Lifschitz 1988) as-well-as the three-valued one of (Przymusinski 1990), retaining their desirable properties. Due to the use of AFT, we also get for free alternative semantics for higher-order logic programs, namely supported model, Kripke-Kleene, and well-founded. Additionally, we define a broad class of stratified higher-order logic programs and demonstrate that they have a unique two-valued higher-order stable model which coincides with the well-founded semantics of such programs. We provide a number of examples in different application domains, which demonstrate that higher-order logic programming under the stable model semantics is a powerful and versatile formalism, which can potentially form the basis of novel ASP systems.

本研究解决了高阶逻辑程序中缺乏稳定模型语义的问题。作者提出了一种基于近似不动点理论的新语义，这种语义不仅推广了经典的两值和三值稳定模型语义，还提供了多种替代语义。研究的关键发现是，广泛的分层高阶逻辑程序具有唯一的两值稳定模型，这可能为新型的答案集编程系统奠定基础。

高阶逻辑程序的稳定模型语义