From Conventional to Institution-Independent Logic Programming. / Tutu, Ionut; Fiadeiro, José Luiz.

In: Journal of Logic and Computation, Vol. 27, No. 6, 01.09.2017, p. 1679-1716.

Research output: Contribution to journalArticle

Published

Documents

  • IILP

    Accepted author manuscript, 637 KB, PDF-document

Links

Abstract

We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions such as logic program, clause, query, solution and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We examine properties concerning the satisfaction of quantified sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any particular logical system or construction of logic programs, and describe a general resolution-based procedure for computing solutions to queries. We prove that this procedure is sound; moreover, under additional hypotheses that reflect faithfully properties of actual logic-programming languages, we show that it is also complete.
Original languageEnglish
Pages (from-to)1679-1716
Number of pages37
JournalJournal of Logic and Computation
Volume27
Issue number6
Early online date9 Jun 2015
DOIs
StatePublished - 1 Sep 2017
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 18150435