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

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.

• Type: Conference
• Year: 2004
• Where: ISCIS
• Authors: Baris Sertkaya, Halit Oguztüzün
• Keywords: Formal Concept Analysis, Isabelle/HOL Proof Assistant, ISCIS 2004, Machine-checked Proof