Foundations of Logic Programming in Hybridised Logics

  • Daniel Găină
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9463)


The present paper sets the foundation of logic programming in hybridised logics. The basic logic programming semantic concepts such as query and solutions, and the fundamental results such as the existence of initial models and Herbrand’s theorem, are developed over a very general hybrid logical system. We employ the hybridisation process proposed by Diaconescu over an arbitrary logical system captured as an institution to define the logic programming framework.


  1. 1.
    Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Log. J. IGPL 8(3), 339–365 (2000)MathSciNetCrossRefMATHGoogle Scholar
  2. 2.
    Braüner, T.: Hybrid Logic and its Proof-Theory. Applied Logic Series, vol. 37. Springer, Berlin (2011)CrossRefMATHGoogle Scholar
  3. 3.
    Diaconescu, R.: Institution-independent Ultraproducts. Fundamenta Informaticæ 55(3–4), 321–348 (2003)MathSciNetMATHGoogle Scholar
  4. 4.
    Diaconescu, R.: Herbrand theorems in arbitrary institutions. Inf. Process. Lett. 90, 29–37 (2004)MathSciNetCrossRefMATHGoogle Scholar
  5. 5.
    Diaconescu, R.: Institution-independent Model Theory. Studies in Universal Logic. Birkhäuser, Basel (2008)MATHGoogle Scholar
  6. 6.
    Diaconescu, R.: Quasi-varieties and initial semantics in hybridized institutions. J. Logic Comput. (2014). doi: 10.1093/logcom/ext016
  7. 7.
    Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39(1), 95–146 (1992)MathSciNetCrossRefMATHGoogle Scholar
  8. 8.
    Goguen, J.A., Thatcher, J.W.: Initial algebra semantics. In: SWAT (FOCS), pp. 63–77. IEEE Computer Society (1974)Google Scholar
  9. 9.
    Găină, D., Futatsugi, K.: Initial semantics in logics with constructors. J. Log. Comput. 25(1), 95–116 (2015). Scholar
  10. 10.
    Găină, D., Futatsugi, K., Ogata, K.: Constructor-based Logics. J. Univ. Comput. Sci. 18(16), 2204–2233 (2012)MathSciNetMATHGoogle Scholar
  11. 11.
    Găină, D., Petria, M.: Completeness by Forcing. J. Log. Comput. 20(6), 1165–1186 (2010)MathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    Lloyd, J.: Foundation of Logic Programming. Springer, Berlin (1987)CrossRefGoogle Scholar
  13. 13.
    Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 283–297. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  14. 14.
    Schurz, G.: Combinations and completeness transfer for quantified modal logics. Log. J. IGPL 19(4), 598–616 (2011). Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Open Access This chapter is distributed under the terms of the Creative Commons Attribution Noncommercial License, which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.

Authors and Affiliations

  1. 1.Research Center for Software VerificationJapan Advanced Institute of Science and Technology (JAIST)NomiJapan

Personalised recommendations