Skip to main content
SpringerLink
Log in

Completeness and Decidability Results for Hybrid(ised) Logics

  • Conference paper
  • First Online:
Book cover Formal Methods: Foundations and Applications (SBMF 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8941))

Included in the following conference series:

Abstract

Adding to the modal description of transition structures the ability to refer to specific states, hybrid(ised) logics provide an interesting framework for the specification of reconfigurable systems. The qualifier ‘hybrid(ised)’ refers to a generic method of developing, on top of whatever specification logic is used to model software configurations, the elements of an hybrid language, including nominals and modalities. In such a context, this paper shows how a calculus for a hybrid(ised) logic can be generated from a calculus of the base logic and that, moreover, it preserves soundness and completeness. A second contribution establishes that hybridising a decidable logic also gives rise to a decidable hybrid(ised) one. These results pave the way to the development of dedicated proof tools for such logics used in the design of reconfigurable systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics. Elsevier (2006)

    Google Scholar 

  2. Baltazar, P.: Probabilization of logics: Completeness and decidability. Logica Universalis 7(4), 403–440 (2013)

    Article  MathSciNet  Google Scholar 

  3. Braüner, T.: Proof-Theory of Propositional Hybrid Logic. Hybrid Logic and its Proof-Theory (2011)

    Google Scholar 

  4. Caleiro, C., Sernadas, C., Sernadas, A.: Parameterisation of logics. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 48–63. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Diaconescu, R.: Institution-independent Model Theory. Birkhäuser, Basel (2008)

    MATH  Google Scholar 

  6. Diaconescu, R.: Institutional semantics for many-valued logics. Fuzzy Sets Syst. 218, 32–52 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  7. Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theor. Comput. Sci. 379(1–2), 210–230 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  8. Fiadeiro, J., Sernadas, A.: Structuring theories on consequence. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 44–72. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  9. Finger, M., Gabbay, D.: Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1(3), 203–233 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  10. Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39, 95–146 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  11. Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987 and CFLP 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987)

    Google Scholar 

  12. Hoffmann, G., Areces, C.: Htab: a terminating tableaux system for hybrid logic. Electr. Notes Theor. Comput. Sci. 231, 3–19 (2009)

    Article  MathSciNet  Google Scholar 

  13. Madeira, A., Faria, J.M., Martins, M.A., Barbosa, L.S.: Hybrid specification of reactive systems: an institutional approach. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 269–285. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Neves, R., Madeira, A., Martins, M.A., Barbosa, L.S.: Hybridisation at work. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 340–345. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Rasga, J., Sernadas, A., Sernadas, C.: Importing logics: Soundness and completeness preservation. Studia Logica 101(1), 117–155 (2013)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HASLab INESC TEC and University of Minho, Braga, Portugal

    Renato Neves & Luís S. Barbosa

  2. CIDMA - Department of Mathematics, University of Aveiro, Aveiro, Portugal

    Manuel A. Martins

Authors
  1. Renato Neves
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manuel A. Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Luís S. Barbosa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Renato Neves .

Editor information

Editors and Affiliations

  1. Universidade Federal Fluminense, Niterói, Brazil

    Christiano Braga

  2. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Neves, R., Martins, M.A., Barbosa, L.S. (2015). Completeness and Decidability Results for Hybrid(ised) Logics. In: Braga, C., Martí-Oliet, N. (eds) Formal Methods: Foundations and Applications. SBMF 2014. Lecture Notes in Computer Science(), vol 8941. Springer, Cham. https://doi.org/10.1007/978-3-319-15075-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15075-8_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15074-1

  • Online ISBN: 978-3-319-15075-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation