Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL | SpringerLink
Skip to main content
Springer Nature Link
Log in

Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL

  • Conference paper
Computer and Information Sciences - ISCIS 2004 (ISCIS 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3280))

Included in the following conference series:

Abstract

This paper presents a machine-checked proof of the Basic Theorem on Concept Lattices, which appears in the book “Formal Concept Analysis” by Ganter and Wille, in the Isabelle/HOL Proof Assistant. As a by-product, the underlying lattice theory by Kammueller has been extended.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 17159
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 21449
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 21–38. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Davey, B.A., Priestley, H.A.: Introduction to lattices and order, 2nd edn. Cambridge University Press, Cambridge (2002)

    MATH  Google Scholar 

  3. Ganter, B., Wille, R.: Applied lattice theory: formal concept analysis (1997), http://www.math.tu-dresden.de/~ganter/concept.ps

  4. Ganter, B., Wille, R.: Formal concept analysis—Mathematical foundations. Springer, Heidelberg (1999)

    MATH  Google Scholar 

  5. Kammueller, F.: Theory Tarski (1999), http://isabelle.in.tum.de/library/HOL/ex/Tarski.html

  6. Krohn, U., Davies, N.J., Weeks, R.: Concept lattices for knowledge management. BT Technology Journal 17 (1999)

    Google Scholar 

  7. Nipkow, T., Paulson, L.C., Wenzel, M.: A proof assistant for higher-order logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  8. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle’s logics: HOL, http://isabelle.in.tum.de/doc/logics-HOL.pdf

  9. Park, Y.: Software retrieval by samples using concept analysis. Journal of Systems and Software 1 (2000)

    Google Scholar 

  10. Paulson, L.C.: Isabelle: A generic theorem prover. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, London (1990)

    Google Scholar 

  11. Paulson, L.C.: The Isabelle reference manual, http://isabelle.in.tum.de/doc/ref.pdf

  12. Puitg, F., Dufourd, J.F.: Formalizing mathematics in higher-order logic: A case study in geometric modelling. Theoretical Computer Science 234 (2000)

    Google Scholar 

  13. Rudnicki, P.: An overview of the Mizar project, http://mizar.org/project/bibliography.html

  14. Schwarzweller, C.: Mizar formalization of concept lattices. Mechanized Mathematics and its Applications 1 (2000)

    Google Scholar 

  15. Sertkaya, B.: Proof of the basic theorem on concept lattices in Isabelle/HOL. M.Sc. thesis, Department of Computer Engineering, Middle East Technical University, Ankara, Turkey (2003)

    Google Scholar 

  16. Wenzel, M.: Isabelle/Isar reference manual, http://isabelle.in.tum.de/doc/isar-ref.pdf

  17. Wenzel, M.: Isabelle/Isar—A versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München (2002), http://tumb1.biblio.tu-munchen.de/publ/dis/in/2002/wenzel.html

  18. Wille, T.: Concept lattices and conceptual knowledge systems. Computers & Mathematics with Applications (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Theoretical Computer Science, Dresden University of Technology, Dresden, Germany

    Barış Sertkaya

  2. Department of Computer Engineering, Middle East Technical University, Ankara, Turkey

    Barış Sertkaya & Halit Oğuztüzün

Authors
  1. Barış Sertkaya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Halit Oğuztüzün
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Bilkent University, TR-06800, Bilkent, Ankara, Turkey

    Cevdet Aykanat

  2. No Affiliation,  

    Tuǧrul Dayar

  3. Department of Computer Engineering, Bilkent University, 06800, Bilkent, Ankara, Turkey

    İbrahim Körpeoğlu

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sertkaya, B., Oğuztüzün, H. (2004). Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL. In: Aykanat, C., Dayar, T., Körpeoğlu, İ. (eds) Computer and Information Sciences - ISCIS 2004. ISCIS 2004. Lecture Notes in Computer Science, vol 3280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30182-0_98

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30182-0_98

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23526-2

  • Online ISBN: 978-3-540-30182-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation