Kategori Teorisi Resimlerle: Mantık (2021)

 (abuseofnotation.github.io)
2 puan yazan GN⁺ 2024-10-27 | 1 yorum | WhatsApp'ta paylaş
  • Mantık, doğru kabul edilen atomik önermelerden başlayıp and, or, implies gibi işleçlerle daha büyük önermeler kurar; kategori teorisinde olduğu gibi bileşim merkezî önemdedir
  • Klasik mantık, önermeleri doğru/yanlış Boolean değerleri olarak, mantıksal işleçleri de Boolean fonksiyonları olarak yorumlar; doğruluk tablolarıyla değilleme, mantıksal ve, mantıksal veya, çıkarım ve eşdeğerliği ele alır
  • Sezgiselci mantığın BHK yorumu, önermeleri kanıtı olan nesneler olarak görür; A ∧ B bir kanıt çifti, A → B ise A kanıtını B kanıtına dönüştüren bir fonksiyon olarak yorumlanır
  • Bazı kategorilerde nesneler önermelere, morfizmler kanıtlara karşılık gelir; sıralarda A ≤ B, A → B anlamına gelen bir preorder veya partial order olarak görünür
  • Sezgiselci mantık, sıralama kuramında Heyting cebirine, genel kategori teorisinde ise bicartesian closed category'ye karşılık gelir; mantıksal ve, mantıksal veya, doğru, yanlış ve çıkarım sırasıyla meet/join, terminal/initial, exponential object'e karşılık gelir

Önermelerden başlayan mantık

  • Mantık, gözlemden bağımsız olarak kendi içinde tutarlı biçimsel kuralları ele alır; bir şeyi bildiğimizde başka bir şeyin doğru olduğu sonucuna varma ya da bunu kanıtlama sistemidir
  • Matematiksel teoriler, mantığa ek tanımların eklendiği yapılar olarak görülebilir
    • Küme teorisi, standart mantık aksiyomlarına küme üyelik ilişkisi adlı ilkel kavram eklenerek tanımlanabilir
  • Mantığa başlamak için doğru veya yanlış olarak kabul edilen bir başlangıç önerme kümesi gerekir
    • Bunlara öncül, atomik önerme veya primary proposition denir
  • İki veya daha fazla önerme, and, or, implies/entails gibi mantıksal işleçler ile tek bir bileşik önerme hâline gelir
    • ∧, and anlamına gelir
    • ∨, or anlamına gelir
    • →, follows ya da çıkarımı ifade eder
  • Bileşik önermeler de atomik önermeler gibi yeniden başka önermelerle birleştirilebilir

Modus ponens ve tautolojiler

  • Modus ponens, A doğruysa ve A → B doğruysa B'nin de doğru olduğunu söyleyen eski bir mantık kalıbıdır
    • Biçimi (A ∧ (A ⇒ B)) → B şeklindedir
    • “Sokrates insandır ve insan olan ölümlüyse, Sokrates ölümlüdür” gibi bir örnekle ifade edilir
  • Mantık yalnızca tek tek işleçlerle değil, birden çok mantıksal işlecin birleşimleri ve ilişkileriyle ilgilenir
    • and ile implies arasındaki ilişki modus ponens'te görünür
    • and ile or arasındaki dağılım yasası da temel ilgi alanlarından biridir
  • Tautoloji, bileşen önermelerin doğru/yanlış değerlerinden bağımsız olarak her zaman doğru olan önermedir
    • Modus ponens'te A ve B doğru da olsa yanlış da olsa tüm formül her zaman doğrudur
    • Her zaman yanlış olan önermeye çelişki denir
    • Bir tautolojiye not eklerseniz çelişki olur; bir çelişkiye not eklerseniz tautoloji olur
  • Değere göre doğru ya da yanlış olması değişen önermelere contingent statement denir; bunlar mantığın ana ilgi alanının dışındadır
  • En basit tautoloji, her önermenin kendisini ima ettiğini söyleyen özdeşlik ilkesidir

Aksiyom şemaları ve mantık sistemleri

  • Tautolojiler, aksiyom şemalarının ve çıkarım kurallarının temelini oluşturur
  • Aksiyom şeması, yer tutucular içeren bir formüldür; bu yer tutucular önermelerle değiştirilerek somut önermeler elde edilebilir
    • Modus ponens'te renkler ya da somut önermeler çıkarıldığında geriye genel yapı kalır
    • Bu yapıya atomik ya da bileşik önermeler yerleştirilerek belirli bir modus ponens önermesi kurulabilir
  • Çıkarım kuralları neredeyse aksiyom şemalarıyla aynı biçimde yazılabilir; aksiyom şemaları da çıkarım kuralları gibi uygulanabilir
  • Her tautoloji bir aksiyom şeması olarak kullanılabilir
  • Mantık sistemi ya da biçimsel sistem, aksiyom şemaları ile çıkarım kurallarının bir koleksiyonudur ve bunların uygulanmasıyla mümkün olan tüm önermeleri üretir
    • Örnek olarak, beş aksiyom şeması ve modus ponens çıkarım kuralından oluşan bir sistem sunulur
    • Böyle bir mantık sisteminin tam olması, Gödel'in tamlık teoremi ile ilişkilidir

Klasik mantığın doğruluk-fonksiyonu yorumu

  • Klasik mantık, her önermenin ya doğru ya da yanlış olduğu ikiliğe dayanır
  • Klasik yorumda önermeler ve işleçler şöyle tanımlanır
    • Önermeler, doğru veya yanlış olan Boolean değerleri gibidir
    • Mantıksal işleçler, bir veya daha fazla Boolean değeri alıp Boolean değeri döndüren fonksiyonlardır
  • Değilleme ¬p, tekli bir işlemdir; doğruyu yanlışa, yanlışı doğruya çevirir
    • Aynı şey doğruluk tablosu ile de gösterilebilir
    • Çifte değillemenin kaldırılması, değilleme iki kez uygulandığında başlangıçtaki değere dönüldüğü gösterilerek kanıtlanır
  • and, iki Boolean değeri alır ve yalnızca ikisi de doğruysa doğru döndürür
    • p ∧ q → p
    • p ∧ q → q
  • or, iki Boolean değerden en az biri doğruysa doğru döndürür
    • p → p ∨ q
    • q → p ∨ q
  • implies ya da material condition, p → q şeklinde yazılır ve yalnızca p doğruyken q yanlışsa yanlıştır
    • Klasik mantıkta p → q, ¬p ∨ q doğru olduğunda aynı şeydir
  • if and only if ya da iff, iki önerme aynı değeri taşıdığında doğrudur
    • P ↔ Q, P → Q ∧ Q → P ile eşdeğerdir
  • Doğruluk tablolarının yanı sıra aksiyomlar ve çıkarım kurallarıyla da p → q ile ¬p ∨ q eşdeğerliği kanıtlanabilir
    • Tam bir eşdeğerlik kanıtı için iki yönlü ispat gerekir

Sezgiselci mantık ve BHK yorumu

  • Sezgiselci mantık, kanıtı evrensel bir gerçeğin keşfi değil, bir inşa olarak görür
  • Bu bakışta her önermenin zorunlu olarak doğru ya da yanlış olduğu ikiliği kullanılamaz
    • Bazı önermeler, yanlış oldukları için değil, verilen mantık sisteminin kapsamı dışında kaldıkları için kanıtlanamayabilir
    • İkiz asallar varsayımı buna sık verilen bir örnektir
  • Brouwer–Heyting–Kolmogorov (BHK) yorumunda odak önermelerden çok kanıtlardadır
    • Önerme, kanıtı bulunan şeydir
    • Mantıksal işleçler, başka kanıtlardan kanıt üreten inşalardır
  • A ∧ B'nin kanıtı, A'nın kanıtı ile B'nin kanıtından oluşan bir çift, yani product'tır
  • A → B, A kanıtını B kanıtına dönüştüren bir fonksiyonun var olduğu anlamına gelir
    • A → B için kanıt kümesi, A'dan B'ye giden fonksiyonlar kümesi, yani hom-set olarak ifade edilir
    • Bu küme boşsa, A kanıtını B kanıtına dönüştürmenin bir yolu yoktur
  • BHK yorumunda ayrı bir iff işleci yoktur ama ok vardır
    • A'dan B'ye ve B'den A'ya fonksiyonlar varsa iki önerme eşdeğer gibi ele alınır
    • Küme bakış açısından bu, iki önermenin kanıt kümelerinin izomorf olmasıdır
  • Değilleme, yalnızca kanıt olmaması anlamına gelmez; A'nın doğru olduğunu varsaydığınızda çelişkiye ulaştığınızı göstermeniz gerekir
    • ⊥, kanıtı olmayan bir formülün kanıtı, yani False veya bottom value rolünü oynar
    • BHK'de ¬A, A → ⊥ diye okunur
    • Küme teorisinde ⊥, boş küme ile gösterilir

Mantığı bir kategori olarak görmek

  • BHK yorumu, mantığı kategori teorisiyle yorumlamak için yüksek seviyeli bir bakış sunar
  • Bazı kategoriler bir mantık sistemi gibi görülebilir
    • Nesneler önermelerdir
    • Morfizmler kanıtlardır
  • Her kategori mantık sistemi olmaz; geçerli mantıksal önermelere karşılık gelen nesnelerin bulunması ve geçersiz önermelere karşılık gelen nesnelerin bulunmaması için belirli koşullar gerekir
  • Bu koşulları sağlayan kategorilere bicartesian closed category denir
  • Basit bir durum olarak önce sıralara bakılırsa, mantık sistemi ile atomik önerme kümesi bir kategori oluşturur
    • A'dan B'ye gitmenin tek bir yolu varsa ya da farkları göz ardı ediliyorsa preorder elde edilir
    • Birbirini gerektiren önermeler eşdeğer sayılırsa partial order elde edilir
    • A ≤ B, A → B anlamına gelir
  • Hasse diyagramında A, B'nin altındaysa A → B geçerlidir

Mantıksal işleçlerin sıralama kuramındaki karşılıkları

  • Mantıktaki and ve or, BHK yorumunda product ve sum olarak görünür; sıralama kuramında ise meet ve join'e karşılık gelir
  • Bir mantık sistemi olabilmesi için herhangi iki önerme and ya da or ile birleştirilebilmelidir; dolayısıyla sıra her eleman çifti için meet ve join içermelidir
    • Böyle sıralara lattice denir
  • and ile or arasındaki önemli yasalardan biri dağılırlıktır
    • Tüm A, B, C için A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C) geçerliyse buna distributive lattice denir
  • Sezgiselci mantığı ifade etmek için lattice'te True ve False'a karşılık gelen elemanların da bulunması gerekir
    • False, ⊥ ile yazılır ve False için bir kanıt varsa her önermenin kanıtlanabileceğini söyleyen patlama ilkesi ile ilişkilidir
    • True, ⊤ ile yazılır; her önermeden çıkar ama kendi başına anlamlı bir içerik üretmez
  • Sıralarda True ve False sırasıyla en büyük nesne ve en küçük nesnedir
    • Kategori teorisi terminolojisinde bunlar terminal object ve initial object'e karşılık gelir
    • En küçük ve en büyük elemanları olan lattice'lere bounded lattice denir

Çıkarım nesnesi ve üstel nesne

  • Bir mantık sistemini ifade eden lattice'te, her A, B çifti için A'nın B'yi ima ettiğini gösteren bir çıkarım nesnesi bulunmalıdır
  • Bu nesne, modus ponens yapısıyla tanımlanır
    • A ∧ (A ⇒ B) → B geçerli olmalıdır
  • Yalnızca bu koşul yeterli değildir
    • A ⇒ B ∧ C ya da A ⇒ B ∧ C ∧ D gibi başka nesneler de aynı yere oturabilir
    • Gerçek A ⇒ B, A ∧ X → B koşulunu sağlayan tüm X'ler içindeki en büyük nesnedir
  • Sıralama kuramında A ⇒ B, exponential element veya relative pseudo-complement olarak adlandırılır
    • A ∧ X ≤ B koşulunu sağlayan en büyük X budur
  • Mantıksal olarak A ∧ X → B koşulunu sağlayan en az içerikli önerme X, çıkarım önermesi A ⇒ B'dir
  • Kategori teorisinde bu, exponential object ya da internal homomorphism object olarak tanımlanır
    • A × X → B biçiminde bir morfizm bulunmalıdır
    • Aynı özelliğe sahip başka her aday nesneden gerçek üstel nesneye giden benzersiz bir morfizm olmalıdır
  • Bu çıkarım nesnesi tanımı sezgiselci mantığa uyar
    • Klasik mantıkta üçüncü hâlin imkânsızlığı nedeniyle A ⇒ B, ¬A ∨ B'ye indirgenir
  • Meet, join ve çıkarım nesnesi gibi A ⇒ B de yalnızca benzersiz bir izomorfizme kadar tanımlıdır

Heyting cebiri ve bicartesian closed category

  • Sezgiselci mantık, True, False, and, or, implies ile kurulur
  • Bu yapı sıra olarak ifade edildiğinde Heyting cebiri elde edilir
    • Join ve meet içerir
    • En büyük ve en küçük nesneyi içerir
    • Çıkarım nesnesi içerir
  • Sezgiselci mantık sistemi bir Heyting cebiri olarak görülebilir
    • and ve or, meet ve join'dir
    • True ve False, en büyük ve en küçük nesnelerdir
    • implies, exponential object'tir
  • Aynı tanım genel kategorilere uyarlanırsa bicartesian closed category elde edilir
    • Product ve coproduct içerir
    • Initial ve terminal object içerir
    • Exponential object içerir
  • Sezgiselci mantık sistemi bicartesian closed category olarak da görülebilir
    • and ve or, product ve coproduct'tur
    • True ve False, terminal ve initial object'tir
    • implies, exponential object'tir
  • Klasik mantığa uyan bir lattice, bounded ve distributive olmasının yanı sıra complemented da olmalıdır
    • Her önerme A için, A ∨ ¬A = 1 ve A ∧ ¬A = 0 koşullarını sağlayan özgün bir ¬A vardır
    • Böyle lattice'lere Boolean cebiri denir

Kategorik mantıkla basit ispatlar

  • A ∨ ⊤ ≅ ⊤, join tanımından doğrudan çıkar
    • Join, iki nesneden büyük ya da onlara eşit olan en küçük üst sınırdır
    • ⊤'dan büyük ya da ona eşit tek nesne ⊤'nin kendisi olduğundan, herhangi bir A ile ⊤'nin join'i ⊤ olur
    • Mantıksal olarak bu, “herhangi bir A veya True, True'dur” tautolojisidir
  • A → B varsa A ∨ B = B olur
    • İki nesneden biri diğerinin üzerindeyse join, yukarıda olan nesnedir
    • Bu, A ∨ ⊤ = ⊤'nin genellemesi olarak görülebilir
    • Çünkü her nesne A için her zaman A → ⊤ geçerlidir
  • Özdeşlik ilkesi, çıkarım nesnesiyle de kanıtlanır
    • A ⇒ A, A ∧ X → A koşulunu sağlayan en büyük X'tir
    • Bu koşul her X için geçerli olduğundan sonuç en büyük nesne ⊤ olur
    • Dolayısıyla A → A her zaman doğrudur
  • Eğer A, tüm modellerde B'yi ima eden bir semantic consequence ise, yani A ⊨ B, o zaman A ⇒ B de ⊤'ye karşılık gelir
    • A zaten B'yi ima ettiğinden A ∧ X → B her X için geçerlidir
    • Buna deduction theorem de denir

Free Heyting cebiri ile mantık kurmak

  • Mantık yapmak için önce problem alanına göre kullanılacak atomik önermeler seçilir
  • Seçilen mantık türü sezgiselci mantıksa, tüm A, B için A ∧ B, A ∨ B gibi bileşik önermelerin grafiği çizilmelidir
  • Bileşik önermelerin bileşimleri de yeniden dahil edilmesi gerektiğinden tam liste sonsuz olur
  • Bir önermenin başka bir önermeyi ima edip etmediği, başlangıç önermesinden çıkan okların yolları izlenerek kontrol edilir
  • Mantık yürütmek, eldeki bilgilerden kanıtlanmak istenen sonuca giden bir yol bulma ya da mevcut kanıtları işleyerek yeni bir kanıt kurma sürecidir
  • Sezgiselci mantıkta genel olarak bir ifadenin aksiyomlardan ulaşılamaz olduğunu, yani kanıtlanamayacağını kanıtlamak zordur

İlgili okumalar

1 yorum

 
GN⁺ 2024-10-27
Hacker News yorumları

  • Bu sayfa gerçekten harika; ilgili konuları çalışırken birçok kez karşıma çıktı
    Yine de öğrenmek için oyumu Milewski'den yana kullanırım. Bunu öğrenmek bir yolculuk ve ct-illustrated'ın yazarı hâlâ o yolculuğun ortasında gibi görünüyor
    Milewski ise bu yolu birçok kez gidip gelmiş biri; bu yüzden kitabı ve blogu iyi bir başlangıç noktası
    https://github.com/hmemcpy/milewski-ctfp-pdf Kitap
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Milewski'nin baştaki on kadar bölümünü okudum; ilk birkaç bölüm gerçekten iyiydi ama kesin tanımlar ve notasyon vermeyen üslubu giderek sinir bozucu hâle geldi
      Hafif ve kesin olmayan düzyazıyla yazılınca her şeyin daha anlaşılır olduğunu düşünüyor gibi; bu da onu başvuru kaynağı olarak neredeyse işe yaramaz kılıyor
      Hiç de öyle değil¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • bartoszmilewski'nin ne demek istediğini anlayamadığım için o kitap bana işe yaramaz görünüyor
      Ama iş yerinde tüm domain modelim için kategori teorisi kullanıyorum

  • Daha önce başka URL'lerde zaten tartışılmıştı
    https://news.ycombinator.com/item?id=28660131 (2 yorum)
    https://news.ycombinator.com/item?id=28660157 (112 yorum)

  • Kitabın başlarında matematiği bilim veya mühendislikle karşılaştırırken şu güzel cümleye rastladım
    “Bu yüzden matematikçiler, yaptıkları işi başka disiplinler için taşıdığı değer açısından sürekli savunmak zorunda kaldıkları tuhaf, hatta benzersiz denebilecek bir konumda bulunurlar. Yeniden vurgulamak gerekirse, başka herhangi bir disiplin için böyle bir şey saçma sayılırdı.”
    Doğrudan para kazandıran sonuçlara dönüşmeyen bir alan okumuş herkesin özdeşleşebileceği bir fikir; sayı tarafında yeteneği olanların da Milton Friedman'ın usturası ile mücadele etmek zorunda kaldığını duymak güzel

    • O hâlde “kültürel çalışmalar” alanındaki birçok projenin aslında doğrudan ABD Savunma Bakanlığı ve Dışişleri Bakanlığı tarafından finanse edilmesi sevindirici
      Bugün “postkolonyalizm” araştırmalarının tamamı Amerikan yumuşak gücünün backend'inden başka bir şey değil; savaş çıktığında muhtemelen sert gücün backend'i de olacak

  • İçteki daireler her zaman dikey olarak ortalanıyorsa daire içinde daire diyagramları ölçek büyüdüğünde pek dayanıklı kalmıyor

  • Kategori teorisini kullanarak, kategori teorisi olmadan çözülemeyecek bir CS/SWE problemini faydalı biçimde çözmüş bir başarı hikâyesi var mı? Monad sayılmaz; çünkü durum gerektirirse doğal olarak icat edilecek bir şeydir
    Lisansüstünde bir yıl çalıştım ama sonunda bıraktım

    • Kategori teorisi olmadan modellenemeyecek bir problem yok
      Kategori teorisinin en temel teoremlerinden biri olan Yoneda leması, kategori diliyle ifade edilen her problemin doğrudan kümeler ve fonksiyonlar diline çevrilebileceğini söyler. Kümelerle tanımlanan tüm matematiksel nesneler için de aynısı geçerli; yani bir adı her zaman tanımıyla değiştirebilirsiniz
      Kategorik dilin bir teorinin örtük çerçevesine katkısı, “kategori” tanımından daha büyük olamaz; o tanım da çok küçüktür. Bu biraz, “bir küme üzerinde birleşme yasası, kapalılık, birim eleman ve ters eleman içeren işlem” daha erişilebilirken neden grup kullanalım diye sormaya benzer
      Soyut cebir, yeterince yaygın olacak kadar basit olan küme üzerindeki işlem türlerini adlandıran bir tanımlar kütüphanesine dayanır. Araçlar veya teknikler, tanımın içinde bulabileceğiniz türden şeyler değildir
      Halkalar, vektör uzayları ve modüller kendi başlarına hemen kabul görürken kategoriler inananlar ve inanmayanlar diye ayrılıyor. Bunun neden olduğunu merak ediyorum
    • Bildiğim en yakın örnek UMAP çalışması
      Leland McInnes ile röportaj yaptığımda, nihai sonucun gerçek kodunda şart olmasa bile kategori teorisinin çeşitli noktaları birleştirmede büyük rol oynadığını ayrıntılı biçimde açıklamıştı
      Önceki son teknoloji yöntem olan t-SNE'ye göre göreli iyileşmeye bakınca, yazılımda kategori teorisini konuşma biçimimize dair eleştirimi yeniden düşünmeme neden olan tek örnek bu
      https://arxiv.org/abs/1802.03426
    • Bu biraz “yürüyerek gidemediğiniz bir yere arabayla gittiğiniz bir başarı hikâyesi var mı?” diye sormaya benziyor
      Kategori teorisi bir dil ve araçtır; bu yüzden kategori teorisinin diliyle söylenebilen şeyler başka dillerle de söylenebilir
      Araba gibi, kullanmayı öğrenirseniz —ki öğrenme eğrisi çok diktir— daha hızlı gidebilirsiniz. İlke olarak, kategori teorisi kavramlarını açıkça anmadan yürüyerek de ulaşılamayacak bir şey yoktur
    • Zaten anladığınız bir şeyi daha genel bir çerçevede yeniden biçimlendirirseniz, gerçekte ne anlama geldiğini daha iyi görür ve özü dağınık ayrıntılardan ayırabilirsiniz
      Benim çok sınırlı anlayışıma göre, nesneleri evrensel özelliklerle karakterize etmek kategori teorisinin önemli bir parçası
      Kategori teorisinin bir başka pratik yararı da bilgisayar bilimcilerin, matematikçilerin ve fizikçilerin birlikte konuşabileceği ortak bir dil sağlamasıdır. Herkes aynı örüntüleri farklı adlarla ve biraz uyumsuz tanımlarla anıyorsa iş birliği kolay olmuyor
    • Topos Institute, kategori teorisi Kool-Aid'ini henüz içmemiş kişilere çok daha şeffaf görüneceğini umdukları yeni bir yazılım geliştiriyor
      Şu anki pre-alpha esas olarak sistem dinamiği modellemesi için, ama hedeflenen çalışma kapsamı için kategorik temelin zorunlu olduğunu düşünüyorum. Herkesin görüşünü memnuniyetle duymak isterim
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Kategori teorisinin faydalı olduğunu düşünüyorum ama henüz bilişim için değil gibi
    Gerçekten ihtiyaç duyduğunuz bir şey yoksa kaçınılmaz olarak zor gelir. Evrensel özellikleri, adjoint functor'ları, Yoneda lemasını gerçekten anlamaya ihtiyaç var mı? Yoksa bunların ne olduğunu öğrenmekte zorlanırsınız
    İlginç biçimde fonksiyonel programlama deneyimi kategori teorisini anlamaya yardımcı oluyor, ama tersi pek geçerli değil. Örneğin parametrik polimorfizm doğal dönüşümlere dair sezgi verir; doğal dönüşümler de kategori teorisinin tüm uygulamalarında merkezîdir
    Kategori teorisinin ikna edici uygulamaları oldukça matematikseldir. Cebirsel topolojide, temsil teorisinde, cebirsel geometride ve klasik olmayan mantıkta bulunabilir

  • Bir hata var
    “Modus ponens, burada A ve B ile gösterilen diğer iki önermeden oluşan bir önermedir; A önermesi doğruysa ve A --> B de doğruysa, yani A, B'yi gerektiriyorsa, B'nin de doğru olduğunu söyler. Örneğin ‘Sokrates insandır’ ve ‘İnsanlar ölür’ü biliyorsak, ‘Sokrates ölür’ü de biliriz.”
    Bu örnek önerme mantığının bir kuralı olan modus ponens'e örnek değil; yüklem mantığı gerektiren kategorik kıyastır

  • Burada “mantık mümkün olanın bilimidir” deniyor; mantık kesin olanın bilimi olmalı değil mi?
    Bence asıl mesele, neyin geçerli olup olmadığını kesin biçimde söyleyebilmeyi sağlamasında

  • Diyagram notasyonu ilginç
    Yazar diyagramların doğruluk koruyan dönüşümleri için çıkarım kuralları da veriyor mu?