Skip to main content
SpringerLink
Log in

Deciding Theoremhood in Fibred Logics Without Shared Connectives

  • Chapter
  • First Online:
The Road to Universal Logic

Part of the book series: Studies in Universal Logic ((SUL))

Abstract

Fibring is a powerful mechanism for combining logics, and an essential tool for designing and understanding complex logical systems. Abstract results about the semantics and proof theory of fibered logics have been extensively developed, including general soundness and completeness preservation results. Decidability, however, a key ingredient for the automated support of the fibered logic, has not deserved similar attention.

In this chapter, we address the problem of deciding theoremhood in fibered logics without shared connectives. Namely, under this assumption, we provide a full characterization of the mixed patterns of reasoning that leads to theorems in the fibered logic, and uses it to prove a general decidability preservation result. The complexity of the decision procedure we obtain is also analyzed.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Beckert, B., Gabbay, D.: Fibring semantic tableaux. In: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX’98, pp. 77–92. Springer, Berlin, Heidelberg (1998)

    Book  Google Scholar 

  2. Béziau, J.-Y.: Universal Logic. In: Childers, T., Majers, O. (eds.) Proceedings of the VIII International Symposium, LOGICA’94, pp. 73–93. Czech Academy of Science, Prague, CZ (1994)

    Google Scholar 

  3. Béziau, J.-Y.: The challenge of combining logics. Log. J. IGPL 19(4), 543 (2011)

    Article  Google Scholar 

  4. Caleiro, C.: Combining Logics. PhD thesis, IST, Universidade Técnica de Lisboa, PT (2000). http://sqig.math.ist.utl.pt/pub/CaleiroC/00-C-PhDthesis.ps

  5. Caleiro, C., Carnielli, W., Rasga, J., Sernadas, C.: Fibring of logics as a universal construction. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 13, pp. 123–187. Springer, Dordrecht (2005)

    Google Scholar 

  6. Caleiro, C. Ramos, J.: Combining classical and intuitionistic implications. In: Konev, B., Wolter, F. (eds.) Frontiers of Combining Systems 07, Lecture Notes in Artificial Intelligence, pp. 118–132. Springer, Berlin, Heidelberg (2007)

    Google Scholar 

  7. Caleiro, C., Ramos, J.: From fibring to cryptofibring: a solution to the collapsing problem. Log. Univers. 1(1), 71–92 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  8. Caleiro, C., Sernadas, A.: Fibring logics. In: Béziau, J.-Y. (ed.) Universal Logic: An Anthology (From Paul Hertz to Dov Gabbay), pp. 389–396. Birkhäuser, Basel (2012)

    Chapter  Google Scholar 

  9. Carnielli, W., Coniglio, M., Gabbay, D., Gouveia, P., Sernadas, C.: Analysis and Synthesis of Logics: How To Cut And Paste Reasoning Systems. Applied Logic, vol. 35. Springer, Dordrecht (2008)

    Google Scholar 

  10. Coniglio, M., Sernadas, A., Sernadas, C.: Preservation by fibring of the finite model property. J. Log. Comput. 21(2), 375–402 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  11. Gabbay, D.: Fibred semantics and the weaving of logics, part 1: Modal and intuitionistic logics. J. Symb. Log. 61(4), 1057–1120 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  12. Gabbay, D.: Fibring Logics. Oxford Logic Guides, vol. 38. Clarendon Press, Oxford (1999)

    Google Scholar 

  13. Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  14. Rasga, J., Sernadas, A., Sernadas, C., Viganò, L.: Fibring labelled deduction systems. J. Log. Comput. 12(3), 443–473 (2002)

    Article  MATH  Google Scholar 

  15. Sernadas, A., Sernadas, C., Caleiro, C.: Fibring of logics as a categorial construction. J. Log. Comput. 9(2), 149–179 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  16. Sernadas, C., Rasga, J., Carnielli, W.: Modulated fibring and the collapsing problem. J. Symbol. Log. 67(4), 1541–1569 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  17. Wójcicki, R.: Theory of Logical Calculi. Kluwer, Dordrecht (1988)

    Book  MATH  Google Scholar 

  18. Zanardo, A., Sernadas, A., Sernadas, C.: Fibring: Completeness preservation. J. Symbol. Log. 66(1), 414–439 (2001)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Acknowledgment

The authors acknowledge the support of EU FP7 Marie Curie PIRSES-GA-2012-318986 project GeTFun: Generalizing Truth-Functionality, and the FEDER/FCT project PEst-OE/EEI/LA0008/2013 and PTDC/EIA-CCO/113033/2009 ComFormCrypt of SQIG-IT. The first author also acknowledges the support of FCT scholarship SFRH/BPD/76513/2011.

Author information

Authors and Affiliations

  1. SQIG – Instituto de Telecomunicações, Dep. Matemática – Instituto Superior Técnico, Universidade de Lisboa, Lisboa, Portugal

    Sérgio Marcelino, Carlos Caleiro & Pedro Baltazar

Authors
  1. Sérgio Marcelino
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carlos Caleiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pedro Baltazar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sérgio Marcelino .

Editor information

Editors and Affiliations

  1. City University of New York, New York, New York, USA

    Arnold Koslow

  2. Federal University of Santa Catarina, Florianópolis, Santa Catarina, Brazil

    Arthur Buchsbaum

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Marcelino, S., Caleiro, C., Baltazar, P. (2015). Deciding Theoremhood in Fibred Logics Without Shared Connectives. In: Koslow, A., Buchsbaum, A. (eds) The Road to Universal Logic. Studies in Universal Logic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-15368-1_18

Download citation

Publish with us

Policies and ethics

Search

Navigation