Revisiting the Institutional Approach to Herbrand's Theorem

Ionut Tutu, Jose Luiz Fiadeiro

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

39 Downloads (Pure)


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
Publication statusPublished - 21 Oct 2015
Event6th Conference on Algebra and Coalgebra in Computer Science - Nijmegen, Netherlands
Duration: 24 Jun 201526 Jun 2015


Conference6th Conference on Algebra and Coalgebra in Computer Science

Cite this