Akademik Veri Yönetim Sistemi
Tezin Türü: Yüksek Lisans
Tezin Yürütüldüğü Kurum: Orta Doğu Teknik Üniversitesi, Türkiye
Tezin Onay Tarihi: 2003
Tezin Dili: İngilizce
Öğrenci: Barış Sertkaya
Eş Danışman: MEHMET HALİT S. OĞUZTÜZÜN, Mehmet Oğuztüzün
Özet:Formel Concept Analysis is an emerging field of applied mathematics based on a lattice-theoretic formalization of the notions of concept and conceptual hierarchy. It thereby facilitates mathematical thinking for conceptual data analysis and knowledge processing. Isabelle, on the other hand, is a generic interactive theory development environment for implementing logical formalisms. It has been instantiated to support reasoning in several object-logics. Specialization of Isabelle for Higher Order Logic is called Isabelle/HOL. Our long term is to formalize the theory of Formal Concept Analysis in Isabelle/HOL. This will provide a mechanized theory for researchers who want to prove their own theorems with utmost precision, and for developers who want to design knowledge processing algorithms. The speccific accomplishment of this thesis is a machinechecked version of the proof of the Basic Theorem of Concept Lattices, which appears in the book "Formal Concept Analysisé by Ganter and Wille. As a by product, the underlying lattice theory by F. Kammueller has been extended.