Revisiting the Institutional Approach to Herbrand's Theorem. / Tutu, Ionut; Fiadeiro, Jose Luiz.

Revisiting the Institutional Approach to Herbrand's Theorem. 2015. p. 304-319.

Research output: Chapter in Book/Report/Conference proceedingConference contribution



  • RIHT

    Accepted author manuscript, 593 KB, PDF-document



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.
Original languageEnglish
Title of host publicationRevisiting the Institutional Approach to Herbrand's Theorem
Number of pages16
StatePublished - 21 Oct 2015
Event6th Conference on Algebra and Coalgebra in Computer Science - Nijmegen, Netherlands


Conference6th Conference on Algebra and Coalgebra in Computer Science
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 26095289