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},
}