Loop-separable programs and their first-order definability

An answer set program with variables is first-order definable on finite structures if the set of its finite answer sets can be captured by a first-order sentence. Characterizing classes of programs that are first-order definable on finite structures is theoretically challenging and of practical relevance to answer set programming. In this paper, we identify a non-trivial class of answer set programs called loop-separable programs and show that they are first-order definable on finite structures.

Authors

• Yin Chen South China Normal University
• Fangzhen Lin
• Yan Zhang
• Yi Zhou Southeast University Key Laboratory of New Generation Artificial Intelligence Technology and Its Interdisciplinary Applications, Ministry of Education, China

Keywords

• Answer set programming
• First-order definability
• Knowledge representation
• Nonmonotonic reasoning