Institution-Independent Logic Programming. / Tutu, Ionut.

2015. 144 p.

Research output: ThesisDoctoral Thesis

Unpublished

Standard

Institution-Independent Logic Programming. / Tutu, Ionut.

2015. 144 p.

Research output: ThesisDoctoral Thesis

Harvard

Tutu, I 2015, 'Institution-Independent Logic Programming', Ph.D., Royal Holloway, University of London.

APA

Vancouver

Author

BibTeX

@phdthesis{269e8d0ea0894a36be83cb77b7c58568,
title = "Institution-Independent Logic Programming",
abstract = "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{\textquoteright}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{\textquoteright}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.",
keywords = "institution theory, logic programming, Herbrand's theorem, service-oriented computing, modularization",
author = "Ionut Tutu",
year = "2015",
language = "English",
school = "Royal Holloway, University of London",

}

RIS

TY - THES

T1 - Institution-Independent Logic Programming

AU - Tutu, Ionut

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - institution theory

KW - logic programming

KW - Herbrand's theorem

KW - service-oriented computing

KW - modularization

M3 - Doctoral Thesis

ER -