Completeness Results for Fibred Parchments

  • C. Caleiro
  • P. Gouveia
  • J. Ramos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


In [6] it was shown that fibring could be used to combine institutions presented as c-parchments, and several completeness preservation results were established. However, their scope of applicability was limited to propositional-based logics. Herein, we extend these results to a broader class of logics, possibly including variables, terms and quantifiers. On the way, we need to consider an enriched notion of proof-calculus that deals explicitly with the substitution provisos that often appear in schematic inference rules. For illustration of the concepts, constructions and results, we shall adopt modal first-order logic as a working example.


Modal Logic Inference Rule Completeness Result Schema Variable Closure Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andréka, H., Németi, I., Sain, I.: Algebraic logic. In: Handbook of Philosophical Logic, 2nd edn., vol. 2. Kluwer Academic Publishers, Dordrecht (2001)Google Scholar
  2. 2.
    Birkhoff, G.: Lattice Theory. AMS Colloquium Publications (1967)Google Scholar
  3. 3.
    Blackburn, P., Rijke, M.: Why combine logics? Studia Logica 59(1), 5–27 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Blok, W., Pigozzi, D.: Algebraizable Logics, vol. 77. Memoires AMS (1989)Google Scholar
  5. 5.
    Caleiro, C.: Combining Logics. PhD thesis, Universidade Técnica de Lisboa (2000)Google Scholar
  6. 6.
    Caleiro, C., Mateus, P., Ramos, J., Sernadas, A.: Combining logics: Parchments revisited. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 48–70. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Coniglio, M.E., Sernadas, A., Sernadas, C.: Fibring logics with topos semantics. Journal of Logic and Computation (in print)Google Scholar
  8. 8.
    Diaconescu, R.: Grothendieck institutions. App. Cat. Str. 10(4), 383–402 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Gabbay, D.: Fibred semantics and the weaving of logics: part 1. Journal of Symbolic Logic 61(4), 1057–1120 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Goguen, J., Burstall, R.: A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In: Poigné, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 313–333. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  11. 11.
    Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Hughes, G., Cresswell, M.: A New Introduction to Modal Logic. Routledge, New York (1996)CrossRefzbMATHGoogle Scholar
  13. 13.
    Kracht, M., Kutz, O.: The semantics of modal predicate logic I: Counter-part frames. In: Advances in Modal Logic. CSLI, vol. 3 (2002)Google Scholar
  14. 14.
    Mendelson, E.: Introduction to Mathematical Logic. van Nostrand, D. (1979)Google Scholar
  15. 15.
    Meseguer, J.: General logics. In: Proceedings of the Logic Colloquium 1987, pp. 275–329. North-Holland, Amsterdam (1989)Google Scholar
  16. 16.
    Mossakowski, T.: Using limits of parchments to systematically construct institutions of partial algebras. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 379–393. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  17. 17.
    Mossakowski, T., Tarlecki, A., Pawłowski, W.: Combining and representing logical systems. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 177–196. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  18. 18.
    Mossakowski, T., Tarlecki, A., Pawłowski, W.: Combining and representing logical systems using model-theoretic parchments. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 349–364. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  19. 19.
    Pawłowski, W.: Presenting and combining inference systems. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 409–424. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Sernadas, A., Sernadas, C., Caleiro, C.: Fibring of logics as a categorial construction. Journal of Logic and Computation 9(2), 149–179 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Sernadas, A., Sernadas, C., Caleiro, C., Mossakowski, T.: Categorial fibring of logics with terms and binding operators. In: Frontiers of Combining Systems 2, pp. 295–316. Research Studies Press (2000)Google Scholar
  22. 22.
    Sernadas, A., Sernadas, C., Zanardo, A.: Fibring modal first-order logics: Completeness preservation. Logic Journal of the IGPL 10(4), 413–451 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Sernadas, C., Rasga, J., Carnielli, W.A.: Modulated fibring and the collapsing problem. Journal of Symbolic Logic 67(4), 1541–1569 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  25. 25.
    Zanardo, A., Sernadas, A., Sernadas, C.: Fibring: Completeness preservation. Journal of Symbolic Logic 66(1), 414–439 (2001)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • C. Caleiro
    • 1
  • P. Gouveia
    • 1
  • J. Ramos
    • 1
  1. 1.CLC – Departamento de MatemáticaIST – UTLLisboaPortugal

Personalised recommendations