From conventional to institution-independent logic programming

Research output: Contribution to journalArticlepeer-review

202 Downloads (Pure)


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 pages38
JournalJournal of Logic and Computation
Issue number6
Early online date4 Jun 2015
Publication statusPublished - 1 Sept 2017

Cite this