Proof of the basic theorem on concept lattices in Isabelle/HOL
COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS, vol.3280, pp.976-985, 2004 (SCI-Expanded, Scopus)
- Publication Type: Article / Article
- Volume: 3280
- Publication Date: 2004
- Doi Number: 10.1007/978-3-540-30182-0_98
- Journal Name: COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS
- Journal Indexes: Science Citation Index Expanded (SCI-EXPANDED), Scopus
- Page Numbers: pp.976-985
- Open Archive Collection: AVESIS Open Access Collection
- Middle East Technical University Affiliated: Yes
Abstract
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.