From conventional to institution-independent logic programming

Ionut Tutu, José Luiz Fiadeiro

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)

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

Keywords

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

Fingerprint

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

Cite this