Geri Dön

Proof of the theorem on concept lattices in Isabelle / HOL

Kavram örgüleri hakkında temel teoremin Isabelle / HOL'da ispatı

  1. Tez No: 143253
  2. Yazar: BARIŞ SERTKAYA
  3. Danışmanlar: YRD. DOÇ. HALİT OĞUZTÜZÜN, YRD. DOÇ. ANDREAS TİEFENBACH
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Formal Kavram Analizi, Isabelle, Yüksek Dereceli Mantık, Formelleştirilmiş Matematik, Formal Concept Analysis, Isabelle, Higher Order Logic, Formalized Math ematics
  7. Yıl: 2003
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 84

Özet

Formal Kavram Analizi, uygulamalı matematiğin gelişmekte olan bir dalıdır. Kavramlar ve kavramların hiyerarşisinin örgü kuramı temellerine dayandırılarak matematiksel olarak formalize edilmesini amaçlar. Böylece kavramsal veri analizi ve bilgi işlemenin matematiksel düşünme yöntemini sağlar. Isabelle, mantıksal formalizasyon yapmak için kullanılan jenerik bir kuram geliştirme ortamıdır. Çeşitli mantıklarda çıkarım yapmayı destekler. Isabelle'in yüksek dereceli mantık için özelleşmiş haline Isabelle/HOL denir. Bu çalışmanın uzun vadeli amacı Formal Kavram Analizi kuramının Isabelle/HOL ortamında formalize edilmesidir. Formalizasyon, Formal Kavram Analizi konusunda kendi teoremlerini ispatlamak isteyen araştırmacılara ve bilgi işleme algoritmaları tasar lamak isteyen geliştiricilere bilgisayar tarafından kontrol edilmiş bir kuram sunmayı amaçlamaktadır. Bu çalışmanın belirgin başarısı, Ganter ve Wille tarafından yazılmış olan Formal Concept Analysis kitabındaki Kavram Örgüleri Hakkındaki Temel Teo remin bilgisayara kontrol ettirilmiş olmasıdır. Çalışmanın yan ürünü olarak F. Kam- rnueller tarafından geliştirilmiş olan örgü kuramı genişletilmiştir.

Özet (Çeviri)

Formal 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 goal is to formalize the theory of Formal Concept Analysis in Is abelle/HOL. This will provide a mechanized theory for researchers who want to prove then own theorems with utmost precision, and for developers who want to design knowl edge processing algorithms. The specific accomplishment of this thesis is a machine- checked 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.

Benzer Tezler

  1. Kafeslerde türev

    The derivate notion on lattices

    NUR KAYANSELÇUK

    Yüksek Lisans

    Türkçe

    Türkçe

    2014

    MatematikYaşar Üniversitesi

    Matematik Ana Bilim Dalı

    PROF. DR. MEHMET TERZİLER

  2. İkili sürekli gerçel di-fonksiyon uzayları ve gerçel tıkızlık

    Spaces of bicontinuous real difunctions and real compactness

    FİLİZ YILDIZ

    Doktora

    Türkçe

    Türkçe

    2006

    MatematikHacettepe Üniversitesi

    Matematik Ana Bilim Dalı

    PROF.DR. LAWRENCE MİCHAEL BROWN

  3. Invariant subspaces of positive operators on banach lattices

    Banach örgüleri üzerindeki pozitif operatörlerin değişmez altuzayları

    MERT ÇAĞLAR

    Yüksek Lisans

    İngilizce

    İngilizce

    2001

    MatematikOrta Doğu Teknik Üniversitesi

    Matematik Ana Bilim Dalı

    DOÇ. DR. ZAFER ERCAN

  4. Fuzzy topolojik uzaylarında kompaktlık

    Compactness in fuzzy topological spaces

    SERAP YILMAZ

    Yüksek Lisans

    Türkçe

    Türkçe

    1998

    MatematikKaradeniz Teknik Üniversitesi

    Matematik Ana Bilim Dalı

    PROF. DR. ALİ BÜLBÜL

  5. On maharam operators

    Maharam operatörler

    ZEYNEP ERCAN

    Yüksek Lisans

    İngilizce

    İngilizce

    2014

    Matematikİstanbul Teknik Üniversitesi

    Matematik Ana Bilim Dalı

    PROF. DR. FATMA ÖZDEMİR

    PROF. DR. ÖMER GÖK