Document Open Access Logo

Revisiting the Institutional Approach to Herbrand’s Theorem

Authors Ionut Tutu, José Luiz Fiadeiro

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2015.304.pdf
  • Filesize: 0.55 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Institution theory
  • Substitution systems
  • Herbrand’s theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Ionut Tutu and José Luiz Fiadeiro. Revisiting the Institutional Approach to Herbrand’s Theorem. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 304-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.304

Author Details

Ionut Tutu
José Luiz Fiadeiro

References

  1. Jiri Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories: The Joy of Cats. Dover Publications, 2009. reprint. Google Scholar
  2. Mihai Codescu. The model theory of higher order logic. Master’s thesis, Şcoala Normală Superioară Bucureşti, 2007. Google Scholar
  3. Răzvan Diaconescu. Category-based constraint logic. Mathematical Structures in Computer Science, 10(3):373-407, 2000. Google Scholar
  4. Răzvan Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticae, 55(3-4):321-348, 2003. Google Scholar
  5. Răzvan Diaconescu. Herbrand theorems in arbitrary institutions. Information Processing Letters, 90(1):29-37, 2004. Google Scholar
  6. Răzvan Diaconescu. Institution-Independent Model Theory. Birkhäuser, 2008. Google Scholar
  7. Răzvan Diaconescu. Quasi-Boolean encodings and conditionals in algebraic specification. Journal of Logic and Algebraic Programming, 79(2):174-188, 2010. Google Scholar
  8. Răzvan Diaconescu. Institutional semantics for many-valued logics. Fuzzy Sets and Systems, 218:32-52, 2013. Google Scholar
  9. Daniel Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types theorems, institutionally. Logica Universalis, 8(3-4):469-498, 2014. Google Scholar
  10. Daniel Găină. Foundations of logic programming in hybridised logics. In Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science. Springer, \arip2015. Google Scholar
  11. Joseph A. Goguen and Rod M. Burstall. Institutions: abstract model theory for specification and programming. Journal of the \acntextACM, 39(1):95-146, 1992. Google Scholar
  12. Joseph A. Goguen, Grant Malcolm, and Tom Kemp. A hidden Herbrand theorem: combining the object and logic paradigms. Journal of Logic and Algebraic Programming, 51(1):1-41, 2002. Google Scholar
  13. Joseph A. Goguen and José Meseguer. \acntextEQLOG: Equality, types, and generic modules for logic programming. In Logic Programming: Functions, Relations, and Equations, pages 295-363. Prentice Hall, 1986. Google Scholar
  14. Joseph A. Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, Theory and Practice of Software Development, volume 250 of Lecture Notes in Computer Science, pages 1-22. Springer, 1987. Google Scholar
  15. Jacques Herbrand. Investigations in proof theory. In From Frege to Gödel: A Source Book in Mathematical Logic, pages 525-581. Harvard University Press, 1967. Google Scholar
  16. John W. Lloyd. Foundations of Logic Programming. Springer, 1987. Google Scholar
  17. Manuel A. Martins, Alexandre Madeira, Răzvan Diaconescu, and Luís Soares Barbosa. Hybridization of institutions. In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Algebra and Coalgebra in Computer Science, volume 6859 of Lecture Notes in Computer Science, pages 283-297. Springer, 2011. Google Scholar
  18. José Meseguer. General logics. In Heinz-Dieter Ebbinghaus, José Fernández-Prida, Manuel Garrido, Daniel Lascar, and Mario Rodriquez-Artalejo, editors, Logic Colloquium 1987, volume 129, pages 275-329. Elsevier, 1989. Google Scholar
  19. José Meseguer. Multiparadigm logic programming. In Hélène Kirchner and Giorgio Levi, editors, Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 158-200. Springer, 1992. Google Scholar
  20. Bernhard Möller, Andrzej Tarlecki, and Martin Wirsing. Algebraic specifications of reachable higher-order algebras. In Donald Sannella and Andrzej Tarlecki, editors, Abstract Data Types, volume 332 of Lecture Notes in Computer Science, pages 154-169. Springer, 1987. Google Scholar
  21. Till Mossakowski, Ulf Krumnack, and Tom Maibaum. What is a derived signature morphism? In Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science. Springer, \arip2015. Google Scholar
  22. Fernando Orejas, Elvira Pino, and Hartmut Ehrig. Institutions for logic programming. Theoretical Computer Science, 173(2):485-511, 1997. Google Scholar
  23. Wieslaw Pawlowski. Context institutions. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Specification of Abstract Data Types, volume 1130 of Lecture Notes in Computer Science, pages 436-457. Springer, 1995. Google Scholar
  24. Donald Sannella and Andrzej Tarlecki. Building specifications in an arbitrary institution. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 337-356. Springer, 1984. Google Scholar
  25. Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Springer, 2011. Google Scholar
  26. Traian Florin Şerbănuţă. Institutional concepts in first-order logic, parameterized specification, and logic programming. Master’s thesis, University of Bucharest, 2004. Google Scholar
  27. Andrzej Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33(3):333-360, 1986. Google Scholar
  28. Ionuţ Ţuţu. Comorphisms of structured institutions. Information Processing Letters, 113(22-24):894-900, 2013. Google Scholar
  29. Ionuţ Ţuţu and José L. Fiadeiro. From conventional to institution-independent logic programming. Journal of Logic and Computation, \arip2015. Google Scholar
  30. Ionuţ Ţuţu and José L. Fiadeiro. Service-oriented logic programming. Logical Methods in Computer Science, \arip2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact