Revisiting the institutional approach to Herbrand's theorem

Ionut Ţuţu, José Luiz Fiadeiro (Lead / Corresponding author)

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

1 Citation (Scopus)
23 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 publication6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
EditorsLawrence S. Moss, Pawel Sobocinski
Place of PublicationGermany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH
Number of pages16
ISBN (Electronic)9783939897842
Publication statusPublished - 2015
Event6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 - Nijmegen, Netherlands
Duration: 24 Jun 201526 Jun 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Conference6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015


  • Herbrand's theorem
  • Institution theory
  • Substitution systems

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Revisiting the institutional approach to Herbrand's theorem'. Together they form a unique fingerprint.

Cite this