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 language | English |
---|---|
Pages (from-to) | 1679-1716 |
Number of pages | 38 |
Journal | Journal of Logic and Computation |
Volume | 27 |
Issue number | 6 |
Early online date | 4 Jun 2015 |
DOIs | |
Publication status | Published - 1 Sept 2017 |