Proof of the basic theorem on concept lattices in Isabelle/HOL
COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS, cilt.3280, ss.976-985, 2004 (SCI-Expanded, Scopus)
- Yayın Türü: Makale / Tam Makale
- Cilt numarası: 3280
- Basım Tarihi: 2004
- Doi Numarası: 10.1007/978-3-540-30182-0_98
- Dergi Adı: COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS
- Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
- Sayfa Sayıları: ss.976-985
- Açık Arşiv Koleksiyonu: AVESİS Açık Erişim Koleksiyonu
- Orta Doğu Teknik Üniversitesi Adresli: Evet
Özet
This paper presents a machine-checked proof of the Basic Theorem on Concept Lattices, which appears in the book "Formal Concept Analysis" by Canter and Wille, in the Isabelle/HOL Proof Assistant. As a by-product, the underlying lattice theory by Kammueller has been extended.