License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2015.304
URN: urn:nbn:de:0030-drops-55419
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5541/
Go to the corresponding LIPIcs Volume Portal

Tutu, Ionut ; Fiadeiro, José Luiz

Revisiting the Institutional Approach to Herbrand’s Theorem

pdf-format:
21.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{tutu_et_al:LIPIcs:2015:5541,
  author =	{Ionut Tutu and Jos{\'e} Luiz Fiadeiro},
  title =	{{Revisiting the Institutional Approach to Herbrand’s Theorem}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{304--319},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Lawrence S. Moss and Pawel Sobocinski},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5541},
  URN =		{urn:nbn:de:0030-drops-55419},
  doi =		{10.4230/LIPIcs.CALCO.2015.304},
  annote =	{Keywords: Institution theory, Substitution systems, Herbrand’s theorem}
}

Keywords: Institution theory, Substitution systems, Herbrand’s theorem
Collection: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
Issue Date: 2015
Date of publication: 28.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI