Institution-Independent Logic Programming

Ionut Tutu

Research output: ThesisDoctoral Thesis

171 Downloads (Pure)


The logic-programming paradigm is a prime example of how the integration of the declarative and the operational aspects of logical systems can be used to provide a unied framework for both specication and programming languages. In essence, programming in logic amounts to giving appropriate axiomatic formalizations of computable functions, which can then be executed by means of carefully designed goal-directed deduction rules. In this thesis, we examine common features of various conventional logicprogramming languages, ranging from the most traditional variant of the paradigm – dened over Horn-clause logic – to rst-order and higher-order equational logic programming. Based on these, we propose an abstract model-theoretic framework that allows us to develop and conduct research into logic programming over an arbitrary logical system, without concrete models, sentences, satisfaction, or deduction, and thus to explore the logicprogramming paradigm for other, less conventional formalisms, like the logic of orchestration schemes used in the context of service-oriented computing. Our study 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 investigate properties concerning the satisfaction of quantied sentences, discuss a variant of Herbrand’s theorem that is not limited in scope to any logical formalism or construction of logic programs, and dene a sound and conditionally complete procedure for computing solutions to queries. Within this setting, we further examine two of the most fundamental aspects of the modularization of logic programs – the preservation and the reection of solutions along morphisms of programs – leading to results that can be applied not only to unstructured logic programs (plain sets of clauses), but also to elaborate module systems.
Original languageEnglish
Awarding Institution
  • Royal Holloway, University of London
  • Fiadeiro, José Luiz, Supervisor
Award date1 Sept 2015
Publication statusUnpublished - 2015


  • institution theory
  • logic programming
  • Herbrand's theorem
  • service-oriented computing
  • modularization

Cite this