From conventional to institution-independent logic programming

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


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 - Sep 2017


  • institution theory
  • substitution systems
  • logic programming
  • Herbrand’s theorem
  • resolution


Dive into the research topics of 'From conventional to institution-independent logic programming'. Together they form a unique fingerprint.

Cite this