diff --git a/metadata/entries/Lovasz_Local.toml b/metadata/entries/Lovasz_Local.toml
--- a/metadata/entries/Lovasz_Local.toml
+++ b/metadata/entries/Lovasz_Local.toml
@@ -1,29 +1,30 @@
title = "General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma"
date = 2023-09-20
topics = [
"Mathematics/Probability theory",
"Mathematics/Combinatorics",
]
abstract = "This entry aims to formalise several useful general techniques for using the probabilistic method for combinatorial structures (or discrete spaces more generally). In particular, it focuses on bounding tools for combinatorics, such as the union and complete independence bounds, and the first formalisation of the pivotal Lovász local lemma. The formalisation focuses on the general lemma, however also proves several useful variations, including the more well-known symmetric version. Both the original formalisation and several of the variations used dependency graphs, which were formalised using Noschinski's general directed graph library. Additionally, the entry provides several useful existence lemmas, required at the end of most probabilistic proofs on combinatorial structures. Finally, the entry includes several significant extensions to the existing probability libraries, particularly for conditional probability (such as Bayes theorem) and independent events. The formalisation is primarily based on Alon and Spencer's textbook \"The Probabilistic Method\", as well as Zhao's course notes on the subject."
license = "bsd"
note = ""
[authors]
[authors.edmonds]
email = "edmonds_email"
[contributors]
[notify]
edmonds = "edmonds_email"
[history]
[extra]
[related]
pubs = [
"https://dl.acm.org/doi/book/10.5555/3002498",
- "https://yufeizhao.com/pm/probmethod_notes.pdf",
+ "Lecture notes by Yufei Zhao",
+ "Wikipedia"
]
diff --git a/web/entries/Lovasz_Local.html b/web/entries/Lovasz_Local.html
--- a/web/entries/Lovasz_Local.html
+++ b/web/entries/Lovasz_Local.html
@@ -1,171 +1,173 @@
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma - Archive of Formal Proofs
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma
This entry aims to formalise several useful general techniques for using the probabilistic method for combinatorial structures (or discrete spaces more generally). In particular, it focuses on bounding tools for combinatorics, such as the union and complete independence bounds, and the first formalisation of the pivotal Lovász local lemma. The formalisation focuses on the general lemma, however also proves several useful variations, including the more well-known symmetric version. Both the original formalisation and several of the variations used dependency graphs, which were formalised using Noschinski's general directed graph library. Additionally, the entry provides several useful existence lemmas, required at the end of most probabilistic proofs on combinatorial structures. Finally, the entry includes several significant extensions to the existing probability libraries, particularly for conditional probability (such as Bayes theorem) and independent events. The formalisation is primarily based on Alon and Spencer's textbook "The Probabilistic Method", as well as Zhao's course notes on the subject.
\ No newline at end of file
diff --git a/web/entries/Paraconsistency.html b/web/entries/Paraconsistency.html
--- a/web/entries/Paraconsistency.html
+++ b/web/entries/Paraconsistency.html
@@ -1,193 +1,194 @@
Paraconsistency - Archive of Formal Proofs
Paraconsistency is about handling inconsistency in a coherent way. In
classical and intuitionistic logic everything follows from an
inconsistent theory. A paraconsistent logic avoids the explosion.
Quite a few applications in computer science and engineering are
discussed in the Intelligent Systems Reference Library Volume 110:
Towards Paraconsistent Engineering (Springer 2016). We formalize a
paraconsistent many-valued logic that we motivated and described in a
special issue on logical approaches to paraconsistency (Journal of
Applied Non-Classical Logics 2005). We limit ourselves to the
propositional fragment of the higher-order logic. The logic is based
on so-called key equalities and has a countably infinite number of
truth values. We prove theorems in the logic using the definition of
validity. We verify truth tables and also counterexamples for
non-theorems. We prove meta-theorems about the logic and finally we
investigate a case study.
A double-ended queue (deque) is a queue where one
can enqueue and dequeue at both ends. We define and verify the deque
implementation by Chuang and Goldberg. It is purely
functional and all operations run in constant time.
- Chuang, T.-R., & Goldberg, B. (1993). Real-time deques, multihead Turing machines, and purely functional programming. Proceedings of the Conference on Functional Programming Languages and Computer Architecture. https://doi.org/10.1145/165180.165225
+ Chuang, T.-R., & Goldberg, B. (1993). Real-time deques, multihead Turing machines, and purely functional programming. Proceedings of the Conference on Functional Programming Languages and Computer Architecture - FPCA ’93. https://doi.org/10.1145/165180.165225
We give a simple relation-algebraic semantics of read and write
operations on associative arrays. The array operations seamlessly
integrate with assignments in the Hoare-logic library. Using relation
algebras and Kleene algebras we verify the correctness of an
array-based implementation of disjoint-set forests with a naive union
operation and a find operation with path compression.
\ No newline at end of file
diff --git a/web/theories/paraconsistency/index.html b/web/theories/paraconsistency/index.html
--- a/web/theories/paraconsistency/index.html
+++ b/web/theories/paraconsistency/index.html
@@ -1,83 +1,84 @@
Paraconsistency - Archive of Formal Proofs