Equilibrium Semantics and Strong Equivalence for Higher-Order Logic Programs
2026-06-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors extend an important logical framework called equilibrium logic to handle higher-order Answer Set Programming (ASP), which allows programs to be more expressive. They show that for a specific class of these higher-order programs, there is always one clear, unique solution called an equilibrium model. They also prove that their language can fully describe the meanings of these programs. Most importantly, they generalize a key rule about when two programs can be considered the same (strong equivalence) to this higher-order context, making it easier to verify and optimize complex ASP programs.
Answer Set ProgrammingEquilibrium LogicStrong EquivalenceHigher-Order LogicStratified ProgramEquilibrium ModelProgram TransformationLogical SemanticsDefinabilityExpressiveness
Authors
Angelos Charalambidis, Giannos Chatziagapis, Babis Kostopoulos, Panos Rondogiannis
Abstract
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.