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.
Similar content being viewed by others
References
BAAZ, M., A. CIABATTONI, and C. G. FERMÜLLER, ‘Herbrand's theorem for Prenex Gödel logic and its consequences for theorem proving’, in Proc. of LPAR 2001, LNCS 2250, pp. 201–216, Springer, 2001.
BALDUCCINI, M., M. GELFOND, R. WATSON, and M. NOGUEIRA, ‘The USA-Advisor: A case study in answer set planning’, in Proc. of LPNMR 2001, LNCS 2173, pp. 439–444, Springer, 2001.
BARAL, C., Knowlewdge Representation, Reasoning and Declarative Problem Solving, Cambridge University Press, 2003.
CALIMERI, F., S. GALIZIA, M. RUFFOLO, and P. RULLO, ‘Enhancing disjunctive logic programming for ontology specification’, in Proc. of International Joint Conference on Declarative Programming, AGP'03, Univ. degli Studi di Reggio Calabria, Italy, September 2003.
EITER, T., J. LU, and V. S. SUBRAHMANIAN, ‘A first-order representation of stable models’, AI Communications, 1:53–73, 1998.
GABBAY, D., Semantical Investigations in Heytings Intuitionistic Logic, Vol. 148 of Synthese Library, D. Reidel, 1981.
GELFOND, M., and V. LIFSCHITZ, ‘Classical negation in logic programs and disjunctive databases’, New Generation Computing, 9:365–385, 1991.
GÖDEL, K., ‘Zumintuitionistischen aussagenkalkül’, Anzeiger der Akademie der Wissenschaften Wien, mathematisch, naturwissenschaftliche Klasse, 69:65–66, 1932.
GORANKO, V., ‘The Craig Interpolation Theorem for Propositional Logics with Strong Negation’, Studia Logica 44(3):291–317, 1985.
GÖRNEMANN, S., ‘A logic stronger than intuitionism’, The Journal of Symbolic Logic 36:249–261, 1971.
GUREVICH, Y., ‘Intuitionistic logic with strong negation’, Studia Logica, 36(1–2):49–59, 1977.
HASUO, I., and R. KASHIMA, ‘Kripke completeness of first-order constructive logics with strong negation’, Logic Journal of the IGPL, 11(6):615–646, 2003.
HEYTING, A., ‘Die formalen regeln der intuitionistischen logik’, Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse, pp. 42–56, 1930.
HOSOI, T., ‘The axiomatization of the intermediate propositional systems Sn of Göel’, Journal of the Faculty of Science of the University of Tokio, 13:183–187, 1966.
JANHUMEN, T., I. NIEMELÄ, D. SEIPEL, P. SIMONS, and J.-H. YOU, ‘Unfolding partiality and disjunctions in stable model semantics’, CoRR: cs.AI/0303009, March 2003.
JASPERS, J., Calculi for Constructive Communication, ILLC Dissertation Series 1994-4, ILLC 1994.
DE JONGH, D., and L. HENDRIKS, ‘Characterization of strongly equivalent logic programs in intermediate logics’, Theory and Practice on Logic Programming, 3(3):259–270, June 2002.
KRACHT, M., ‘On extensions of intermediate logics by strong negation’, Journal of Philosophical Logic, 27(1):49–73, 1998.
LEONE, N., G. PFEIFER, W. FABER, T. EITER, G. GOTTLOB, S. PERRI, and F. SCARCELLO, ‘The dlv system for knowledge representation and reasoning’, CoRR: cs.AI/0211004, September 2003.
LIFSCHITZ, V., D. PEARCE, and A. VALVERDE, ‘Strongly equivalent logic programs’, ACM Transactions on Computational Logic, 2(4):526–541, October 2001.
LIFSCHITZ, V., L.R. TANG, and H. TURNER, ‘Nested expressions in logic programs’, Annals of Mathematics and Artificial Intelligence, 25(3–4):369–389, 1999.
ŁUKASIEWICZ, J., ‘Die logik und das grundlagenproblem’, in Les entretiens de Zûrich sur les fondements et la méthode des sciences mathématiques (Zûurich, 1938), pp. 82–100, 1941.
MARKOV, A.A., ‘Konstructivnaja logika’, Usp. Mat. Nauk 5: 1897-188, 1950.
NELSON, D. ‘Constructible falsity’, Journal of Symbolic Logic, 14(2):16–26, 1949.
ONO, H. ‘Model Extension Theorem and Craig's Interpolation Theorem for Intermediate Predicate Logics’, Reports on Mathematical Logic 15:41–58, 1983.
PEARCE, D., ‘Answer Sets and Constructive Logic. Part II: extended logic programs and related nonmonotonic formalisms’, in L. M. Periera and A. Nerode, (eds.), Logic Porgramming and Non-monotonic Reasoning, pp. 457–475, MIT press, 1993.
PEARCE, D., ‘A new logical characterization of stable models and answer sets’, in Proc. of NMELP 96, LNCS 1216, pp. 57–70, Springer, 1997.
PEARCE, D., ‘Fromhere to there: Stable negation in logic programming’, in Dov Gabbay and Heinrich Wansing, (eds.), What is Negation?, pp. 161–181, Kluwer Academic Pub., 1999.
PEARCE, D., ‘Simplifying logic programs under answer set semantics’, in Vladimir Lifschtiz and Bart Demoen, (eds.), Proc. of ICLP04. Springer, 2004, (to appear).
PEARCE, D., and G. Wagner, ‘Reasoning with Negative Information I: Strong Negation in Logic Programs’, in L. Haaparanta, M. Kusch, and I. Niiniluoto, (eds.), Language, Knowledge and Intentionality, Acta Philosophica Fennica 49, Helsinki, 1990
PEARCE, D., and G. Wagner, ‘Logic Programming with Strong Negation’, in P. Schroeder-Heister, (ed.), Extensions of Logic Programming, Springer LNAI 475, 1991.
PEARCE, D., and A. Valverde, ‘Uniform equivalence for equilibrium logic and logic programs’, in Proc. of LPNMR'04, LNAI 2923, pp. 194–206, Springer, 2004.
PEARCE, D., and A. Valverde, ‘Synonymous theories in answer set programming and equilibrium logic’, in Proc. of ECAI 2004 (Valencia, Spain), 2004, (to appear).
RASIOWA, H., An Algebraic Approach to Non-classical Logic PWN, Warsaw and North-Holland, Amsterdam, 1974.
ROUTLEY, R. ‘Semantical Analyses of Propositional Systems of Fitch and Nelson’, Studia Logica 33(3):283–298, 1974.
SIMONS, P., I. NIEMELÄ, and T. SOININEN, ‘Extending and implementing the stable model semantics’, Artificial Intelligence, 138(1–2):181–234, 2002.
SKVORTSOV, D., ‘On Intermediate Predicate Logics of some Finite Kripke Frames, I. Levelwise Uniform Trees’, Studia Logica 77(3):295–323, 2004.
THOMASON, R.H., ‘A Semantical Study of Constructible Falsity’, Zeitschrift für Mathematische Logik 15:247–257, 1969.
VAKARELOV, D., Theory of negation in certain logical systems. Algebraic and semantical approach, Ph.D. dissertation, University of Warsaw, 1976.
VAKARELOV, D., ‘Notes on constructive logic with strong negation’, Studia Logica, 36:89–107, 1977.
VAN DALEN, D., ‘Intuitionistic logic’, in Dov Gabbay and Franz Guenther, (eds.), Handbook of Philosophical Logic, Volume III: Alternatives in Classical Logic, D. Reidel Publishing Co., Dordrecht, 1986.
VOROB'EV, N.N., ‘A constructive propositional calculus with strong negation (in russian)’, Doklady Akademii Nauk SSR, 85:465–468, 1952.
VOROB'EV, N.N., ‘The problem of deducibility in constructive propositional calculus with strong negation (in russian)’, Doklady Akademii Nauk SSR, 85:689–692, 1952.
VOROB'EV, N.N., ‘Constructive propositional calculus with strong negation (in russian)’, Transactions of Steklov's Institute, 72:195–227, 1964.
WAGNER, G., Vivid Logic. Knowledge-Based reasoning with Two Kinds of Negation, Springer LNAI 764, 1994.
WANSING., H., The Logic of Information Structures, Springer LNAI 681, 1993.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Pearce, D., Valverde, A. A First Order Nonmonotonic Extension of Constructive Logic. Stud Logica 80, 321–346 (2005). https://doi.org/10.1007/s11225-005-8473-8
Issue Date:
DOI: https://doi.org/10.1007/s11225-005-8473-8