Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-24T03:43:56.792Z Has data issue: false hasContentIssue false
  • English
  • Français

Encoding hybridized institutions into first-order logic

Published online by Cambridge University Press:  12 November 2014

RĂZVAN DIACONESCU  and
ALEXANDRE MADEIRA
RĂZVAN DIACONESCU
Affiliation:
Simion Stoilow Institute of Mathematics of the Romanian Academy, Bucharest, Romania E-mail: [email protected]
ALEXANDRE MADEIRA
Affiliation:
HASLab/INESC TEC – Universidade do Minho, Braga, Portugal E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A ‘hybridization’ of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By ‘hybridized institutions’ we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated $\mathcal{FOL}$) as a ‘hybridization’ process of abstract encodings of institutions into $\mathcal{FOL}$, which may be seen as an abstraction of the well-known standard translation of modal logic into $\mathcal{FOL}$. The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover, we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to $\mathcal{FOL}$.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 5 , June 2016 , pp. 745 - 788
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aiguier, M. and Diaconescu, R. (2007) Stratified institutions and elementary homomorphisms. Information Processing Letters, 103 (1)5–13.Google Scholar
Areces, C., Blackburn, P. and Delany, S. R. (2001) Bringing them all together. Journal of Logic and Computation, 11 657–669.Google Scholar
Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D. and Tarlecki, A. (2002) CASL: The common algebraic specification language. Theoretical Computer Science 286 (2)153–196.Google Scholar
Béziau, J.-Y. (2006) 13 questions about universal logic. Bulletin of the Section of Logic 35 (2/3)133–150.Google Scholar
Béziau, J.-Y. (ed.) (2012) Universal Logic: An Anthology, Studies in Universal Logic. Springer, Basel.Google Scholar
Blackburn, P. (2000) Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic Journal of IGPL 8 (3)339–365.CrossRefGoogle Scholar
Blackburn, P. and Marx, M. (2002) Tableaux for quantified hybrid logic. In: Egly, U. and Fermüller, C. G. (eds.) TABLEAUX 2002. Springer Lecture Notes in Computer Science 2381 38–52.CrossRefGoogle Scholar
Blackburn, P. and Seligman, J. (1995) Hybrid languages. Journal of Logic, Language and Information 4 (3)251–272.Google Scholar
Blackburn, P. and Tzakova, M. (1999) Hybrid languages and temporal logic. Logic Journal of IGPL 7 (1)27–54.Google Scholar
Braüner, T. (2005) Natural deduction for first-order hybrid logic. Journal of Logic, Language and Information 14 173.Google Scholar
Braüner, T. (2011) Hybrid Logic and its Proof-Theory, Applied Logic Series, volume 37, Springer.Google Scholar
Burstall, R. and Goguen, J. (1980) The semantics of Clear, a specification language. In: Bjorner, D. (ed.) 1979 Copenhagen Winter School on Abstract Software Specification. Springer Lecture Notes in Computer Science 86 292–332.Google Scholar
Carnielli, W., Coniglio, M., Gabbay, D. M., Gouveia, P. and Sernadas, C. (2008) Analysis and Synthesis of Logics How to Cut and Paste Reasoning Systems, Applied Logic – Series, volume 35, Springer.Google Scholar
Cerioli, M. and Meseguer, J. (1997) May I borrow your logic? (transporting logical structures along maps) Theoretical Computer Science 173 311–347.CrossRefGoogle Scholar
Diaconescu, R. (2008) Institution-Independent Model Theory, Birkhäuser.Google Scholar
Diaconescu, R. (2009) An encoding of partial algebras as total algebras. Information Processing Letters 109 (23–24)1245–1251.Google Scholar
Diaconescu, R. (2010) Quasi-boolean encodings and conditionals in algebraic specification. Journal of Logic and Algebraic Programming 79 (2)174–188.Google Scholar
Diaconescu, R. (2011) Coinduction for preordered algebras. Information and Computation 209 (2)108–117.Google Scholar
Diaconescu, R. (2012a) Borrowing interpolation. Journal of Logic and Computation 22 (3)561–586.Google Scholar
Diaconescu, R. (2012b) Interpolation for predefined types. Mathematical Structures in Computer Science 22 (1)1–24.CrossRefGoogle Scholar
Diaconescu, R. (2013) Quasi-varieties and initial semantics in hybridized institutions. Journal of Logic and Computation (DOI:10.1093/logcom/ext016).Google Scholar
Diaconescu, R., Goguen, J. and Stefaneas, P. (1993) Logical support for modularisation. In: Huet, G. and Plotkin, G. (eds.) Logical Environments, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991, Cambridge83–130.Google Scholar
Diaconescu, R. and Stefaneas, P. (2007) Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science 379 (1)210–230.Google Scholar
Finger, M. and Gabbay, D. M. (1992) Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1 (3)203–233.Google Scholar
Goguen, J. and Burstall, R. (1992) Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39 (1)95–146.Google Scholar
Goguen, J. and Roşu, G. (2002) Institution morphisms. Formal Aspects of Computing 13 274–307.Google Scholar
Hodges, W. (1997) A Shorter Model Theory, Cambridge University Press.Google Scholar
Lane, S. M. (1998) Categories for the Working Mathematician, 2nd edition, Springer.Google Scholar
Madeira, A. (2013) Foundations and Techniques for Software Reconfigurability. Ph.D. thesis, Universidades do Minho, Aveiro and Porto (Joint MAP-i Doctoral Programme)Google Scholar
Martins, M. A., Madeira, A., Diaconescu, R. and Barbosa, L. (2011) Hybridization of institutions. In: Corradini, A., Klin, B. and Cîrstea, C. (eds.) Algebra and Coalgebra in Computer Science. Springer Lecture Notes in Computer Science 6859 283–297.Google Scholar
Meseguer, J. (1989) General logics. In: Ebbinghaus, H.-D.et al. (eds.) Proceedings, Logic Colloquium, 1987, North-Holland 275–329.Google Scholar
Mossakowski, T. (1996) Different types of arrow between logical frameworks. In: auf der Heide, F. M. and Monien, B. (eds.) Proceedings of the ICALP 96. Springer-Verlag Lecture Notes in Computer Science 1099 158–169.Google Scholar
Mossakowski, T., Diaconescu, R. and Tarlecki, A. (2009) What is a logic translation? Logica Universalis 3 (1)59–94.Google Scholar
Mossakowski, T., Maeder, C. and Lütich, K. (2007) The heterogeneous tool set. In: Lecture Notes in Computer Science 4424 519–522.Google Scholar
Neves, R., Madeira, A., Martins, M. A. and Barbosa, L. S. (2013) Hybridisation at work. In: Algebra and Coalgebra in Computer Science. Lecture Notes in Computer Science 8089 340–345.CrossRefGoogle Scholar
Passy, S. and Tinchev, T. (1991) An essay in combinatory dynamic logic. Information and Computation 93 (2)263–332.Google Scholar
Petria, M. and Diaconescu, R. (2006) Abstract Beth definability in institutions. Journal of Symbolic Logic 71 (3)1002–1028.Google Scholar
Prior, A. N. (1967) Past, Present and Future, Oxford University Press.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (2012) Foundations of Algebraic Specifications and Formal Software Development, Springer.Google Scholar
Schurz, G. (2011) Combinations and completeness transfer for quantified modal logics. Logic Journal of the IGPL 19 (4)598–616.Google Scholar
Tarlecki, A. (1986) Bits and pieces of the theory of institutions. In: Pitt, D., Abramsky, S., Poigné, A. and Rydeheard, D. (eds.) Proceedings, Summer Workshop on Category Theory and Computer Programming. Springer Lecture Notes in Computer Science 240 334–360.Google Scholar
Tarlecki, A. (1996) Moving between logical systems. In: Haveraaen, M., Owe, O. and Dahl, O.-J. (eds.) Recent Trends in Data Type Specification. Springer Lecture Notes in Computer Science 1130 478–502.CrossRefGoogle Scholar
Tarlecki, A. (2000) Towards heterogeneous specifications. In: Gabbay, D. and van Rijke, M. (eds.) Proceedings, International Conference on Frontiers of Combining Systems, Research Studies Press 337–360.Google Scholar
van Bentham, J. (1988) Modal Logic and Classical Logic, Humanities Press.Google Scholar
Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C. and Topic, D. (2002) Spass version 2.0. In: Proceedings of the 18th International Conference on Automated Deduction, London, UK, Springer-Verlag 275–279.Google Scholar