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

11 Downloads (Pure)

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.

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
Pages304-319
Number of pages16
ISBN (Electronic)9783939897842
DOIs
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
Volume35
ISSN (Print)1868-8969

Conference

Conference6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
CountryNetherlands
CityNijmegen
Period24/06/1526/06/15

Keywords

  • Herbrand's theorem
  • Institution theory
  • Substitution systems

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

Cite this