A First Order Nonmonotonic Extension of Constructive Logic |
| |
Authors: | David Pearce Agustín Valverde |
| |
Institution: | (1) Dept. de Informatica, Estadística y Telemática, Universidad Rey Juan Carlos, C/ Tulipán, 28933 Móstoles, Madrid, Spain;(2) Department of Applied Mathematics, University of Málaga, Bvd. Louis Pasteur s/n, E.T.S.I. Informática, 29071 Málaga, Spain |
| |
Abstract: | Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence
and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look
at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the
answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In
particular, we prove completeness for .rst-order here-and-there logics, and their minimal strong negation extensions, for
both constant and varying domains. We choose the constant domain version, which we denote by QNc5, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic
properties of QNc5, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference. |
| |
Keywords: | Constructive negation here-and-there logic equilibrium logic interpolation answer set programming |
本文献已被 SpringerLink 等数据库收录! |
|