Skip to main content
SpringerLink
Log in

Unifiability and Admissibility in Finite Algebras

  • Conference paper
How the World Computes (CiE 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7318))

Included in the following conference series:

Abstract

Unifiability of finite sets of equations and admissibility of quasiequations in finite algebras are decidable problems, but a naive approach is computationally unfeasible even for small algebras. Algorithms are given here for obtaining more efficient proof systems deciding these problems, and some applications of the algorithms are described.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Morawska, B.: Unification in the description logic EL. Logical Methods in Computer Science 6(3) (2010)

    Google Scholar 

  2. Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol. I, ch. 8, pp. 447–533. Elsevier (2001)

    Google Scholar 

  3. Baaz, M., Fermüller, C.G., Salzer, G.: Automated deduction for many-valued logics. In: Handbook of Automated Reasoning, vol. II, ch.20, pp. 1355–1402. Elsevier Science B.V. (2001)

    Google Scholar 

  4. Babenyshev, S., Rybakov, V., Schmidt, R.A., Tishkovsky, D.: A tableau method for checking rule admissibility in S4. In: Proceedings of UNIF 2009. ENTCS, vol. 262, pp. 17–32 (2010)

    Google Scholar 

  5. Beckert, B., Hähnle, R., Oel, P., Sulzmann, M.: The Tableau-Based Theorem Prover 3 T A P, Version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 303–307. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  6. Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Graduate Texts in Mathematics, vol. 78. Springer, New York (1981)

    Book  MATH  Google Scholar 

  7. Cintula, P., Metcalfe, G.: Structural completeness in fuzzy logics. Notre Dame Journal of Formal Logic 50(2), 153–183 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  8. Cintula, P., Metcalfe, G.: Admissible rules in the implication-negation fragment of intuitionistic logic. Annals of Pure and Applied Logic 162(10), 162–171 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  9. Ghilardi, S.: Unification in intuitionistic logic. Journal of Symbolic Logic 64(2), 859–880 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  10. Ghilardi, S.: Best solving modal equations. Annals of Pure and Applied Logic 102(3), 184–198 (2000)

    Article  MathSciNet  Google Scholar 

  11. Ghilardi, S.: A resolution/tableaux algorithm for projective approximations in IPC. Logic Journal of the IGPL 10(3), 227–241 (2002)

    Article  MathSciNet  Google Scholar 

  12. Gil, A.J., Salzer, G.: Homepage of MUltseq, http://www.logic.at/multseq

  13. Gorbunov, V.A.: Algebraic Theory of Quasivarieties. Springer (1998)

    Google Scholar 

  14. Hähnle, R.: Automated Deduction in Multiple-Valued Logics. OUP (1993)

    Google Scholar 

  15. Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. Journal of Symbolic Logic 66(1), 281–294 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  16. Iemhoff, R., Metcalfe, G.: Proof theory for admissible rules. Annals of Pure and Applied Logic 159(1-2), 171–186 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  17. Jeřábek, E.: Admissible rules of modal logics. Journal of Logic and Computation 15, 411–431 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  18. Jeřábek, E.: Admissible rules of Łukasiewicz logic. Journal of Logic and Computation 20(2), 425–447 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  19. Jeřábek, E.: Bases of admissible rules of Łukasiewicz logic. Journal of Logic and Computation 20(6), 1149–1163 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  20. Metcalfe, G., Röthlisberger, C.: Admissibility in De Morgan algebras. Soft Computing (February 2012)

    Google Scholar 

  21. Olson, J.S., Raftery, J.G.: Positive Sugihara monoids. Algebra Universalis 57, 75–99 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  22. Rybakov, V.: Admissibility of Logical Inference Rules. Studies in Logic and the Foundations of Mathematics, vol. 136. Elsevier, Amsterdam (1997)

    Book  MATH  Google Scholar 

  23. Salzer, G.: Homepage of MUltlog, http://www.logic.at/multlog

  24. Sofronie-Stokkermans, V.: On unification for bounded distributive lattices. ACM Transactions on Computational Logic 8(2) (2007)

    Google Scholar 

  25. Sprenger, M.: Algebra Workbench. Homepage, http://www.algebraworkbench.net

  26. Zach, R.: Proof theory of finite-valued logics. Master’s thesis, Technische Universität Wien (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematics Institute, University of Bern, Sidlerstrasse 5, 3012, Bern, Switzerland

    George Metcalfe & Christoph Röthlisberger

Authors
  1. George Metcalfe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Röthlisberger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Mathematics, University of Leeds, LS2 9JT, Leeds, UK

    S. Barry Cooper

  2. Computer Laboratory, University of Cambridge, Willialm Gates Building, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  3. Institute for Logic, Language and Computation, University of Amsterdam, 1090 GE, Amsterdam, The Netherlands

    Benedikt Löwe

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Metcalfe, G., Röthlisberger, C. (2012). Unifiability and Admissibility in Finite Algebras. In: Cooper, S.B., Dawar, A., Löwe, B. (eds) How the World Computes. CiE 2012. Lecture Notes in Computer Science, vol 7318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30870-3_49

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30870-3_49

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-30869-7

  • Online ISBN: 978-3-642-30870-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation