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

Baris SertkayaBaris Sertkaya, Halit OguztuzunHalit Oguztuzun

Download

Baris Sertkaya, Halit Oguztuzun
Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL
In C. {Aykanat} and T. {Dayar} and I. {Korpeoglu}, eds., Proceedings of the 19th International Symposium on Computer and Information Sciences ({ISCIS2004}), volume 3280 of Lecture Notes in Computer Science, 976--985, 2004. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ SertkayaOguztuzunISCIS2004,
  author = {Baris {Sertkaya} and Halit {Oguztuzun}},
  booktitle = {Proceedings of the 19th International Symposium on Computer and Information Sciences ({ISCIS2004})},
  editor = {C. {Aykanat} and T. {Dayar} and I. {Korpeoglu}},
  pages = {976--985},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL},
  volume = {3280},
  year = {2004},
}