@inproceedings{fb62642c2b444b87aec3933666223e3e,

title = "Revisiting the institutional approach to Herbrand's theorem",

abstract = "More than a decade has passed since Herbrand's theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand's theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution-independent versions of Herbrand's theorem can be obtained as concrete instances of a more general result.",

keywords = "Herbrand's theorem, Institution theory, Substitution systems",

author = "Ionut {\c T}u{\c t}u and Fiadeiro, {Jos{\'e} Luiz}",

year = "2015",

doi = "10.4230/LIPIcs.CALCO.2015.304",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH",

pages = "304--319",

editor = "Moss, {Lawrence S.} and Pawel Sobocinski",

booktitle = "6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)",

address = "Germany",

note = "6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 ; Conference date: 24-06-2015 Through 26-06-2015",

}