Towards a First Order Equilibrium Logic for Nonmonotonic Reasoning

Equilibrium logic, introduced in [20], is a conservative extension of answer set semantics for logic programs to the full language of propositional logic. In this paper we initiate the study of first-order variants of equilibrium logic. In particular, we focus on a quantified version QN₅ of the propositional many-valued logic N₅ of here-and-there with strong negation, and define the condition of equilibrium via a minimal model construction. We verify Skolem forms and Herbrand theorems for QN₅ and show that, like its propositional counterpart, the quantified version of equilibrium logic also conservatively extends answer set semantics.