One of the most significant achievements of equilibrium logic was the characterization of strong equivalence, a property crucial for program transformation and optimization in Answer Set Programming (ASP). While ASP has recently been extended to a higher-order setting to enhance its expressive power, the lack of a comparable purely logical foundation has made verifying strong equivalence for higher-order programs or even proving the correctness of simple program transformations, a difficult challenge. This paper addresses this gap by developing a logical semantics for higher-order ASP by extending the equilibrium logic framework. Within this extended framework we demonstrate that every stratified higher-order logic program possesses a unique equilibrium model. Moreover, we establish definability results demonstrating that the syntax of our higher-order language is sufficiently expressive to capture its semantic domains. Finally, and most importantly, we generalize the classical theorem of strong equivalence to the higher-order setting: we prove that two programs are strongly equivalent if and only if they share the same higher-order models.

翻译：均衡逻辑最重要的成就之一是对强等价性的刻画，这一性质在回答集编程（ASP）的程序转换与优化中至关重要。尽管ASP近期已被扩展到高阶框架以增强其表达能力，但由于缺乏可比较的纯逻辑基础，验证高阶程序的强等价性甚至证明简单程序转换的正确性一直面临困难。本文通过扩展均衡逻辑框架，构建了高阶ASP的逻辑语义，填补了这一空白。在该扩展框架中，我们证明每个分层高阶逻辑程序均存在唯一的均衡模型。此外，我们建立了可定义性结果，证明高阶语言语法具有足够的表达能力来捕获其语义域。最后，也是最重要的，我们将经典的强等价性定理推广到高阶情形：证明两个程序强等价当且仅当它们共享相同的高阶模型。