# Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs

arXiv: https://arxiv.org/abs/1804.08335 · HTML: https://mlsanity.com/paper/1804.08335/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Apr 2018.

## Built on by (most cited first, 5 of 5)

- [Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory](https://mlsanity.com/paper/2104.14789/) (2021)
- [Fixpoint Semantics for Recursive SHACL](https://mlsanity.com/paper/2109.08285/) (2021)
- [Non-Deterministic Approximation Fixpoint Theory and Its Application in Disjunctive Logic Programming](https://mlsanity.com/paper/2211.17262/) (2022)
- [The Stable Model Semantics for Higher-Order Logic Programming](https://mlsanity.com/paper/2408.10563/) (2024)
- [Approximation Fixpoint Theory with Refined Approximation Spaces](https://mlsanity.com/paper/2506.16294/) (2025)

## Abstract (arXiv)

We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs. This paper is under consideration for acceptance in TPLP.