Proof of the basic theorem on concept lattices in Isabelle/HOL

Sertkaya, B; Oguztuzun, MEHMET

doi:10.1007/978-3-540-30182-0_98

Proof of the basic theorem on concept lattices in Isabelle/HOL

Copy For Citation

Sertkaya B., Oguztuzun H.

COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS, vol.3280, pp.976-985, 2004 (SCI-Expanded)

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