Update themes and add content

17 files changed, 92 insertions, 79 deletions

diff --git a/.gitmodules b/.gitmodules
index e5e02d5..0e861c2 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,6 +1,3 @@
-[submodule "themes/hugo-blog-awesome"]
-	path = themes/hugo-blog-awesome
-	url = https://github.com/hugo-sid/hugo-blog-awesome.git
 [submodule "themes/hugo-xmin"]
 	path = themes/hugo-xmin
-	url = https://github.com/yihui/hugo-xmin
+	url = https://git.sr.ht/~ymherklotz/zk-theme
diff --git a/content/zettel/1b1.md b/content/zettel/1b1.md
index 14b0c84..fa8535f 100644
--- a/content/zettel/1b1.md
+++ b/content/zettel/1b1.md
@@ -3,7 +3,7 @@ title = "Guarded commands"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["1d1", "1b2", "1b"]
+backlinks = ["1d1", "1b"]
 forwardlinks = ["1b2"]
 zettelid = "1b1"
 +++
diff --git a/content/zettel/1b2.md b/content/zettel/1b2.md
index 150523f..c0b9e07 100644
--- a/content/zettel/1b2.md
+++ b/content/zettel/1b2.md
@@ -4,7 +4,7 @@ author = "Yann Herklotz"
 tags = []
 categories = []
 backlinks = ["1d1", "1b1"]
-forwardlinks = ["3a", "1b1", "1b3"]
+forwardlinks = ["3a", "1b3"]
 zettelid = "1b2"
 +++
 
@@ -33,39 +33,6 @@ to support a subset of possible recursive functions. Even though these
 are as powerful as loops, it may be more natural to write their
 definitions as a recursive function instead of a loop.
 
-{{< transclude-1 zettel="1b1" >}}
-
-Guarded commands \[2\] are an interesting construct which can be added
-to languages. They look similar to `case` statements, but behave in a
-parallel and nondeterministic way. Each guard has a boolean value
-followed by a program which may be executed if the guard evaluates to
-true. The following shows the main syntax that guards may have.
-
-``` grammar
-e ::= if gc fi | do gc od ...
-
-gc ::= (b e) || gc
-```
-
-One reason these are interesting language constructs, is because they
-allow for the encoding of commands that may be executed when a condition
-is true, but that it isn't necessary. Often, when giving instructions,
-one does not really specify the order, just the commands that should
-eventually be executed.
-
-The guarded commands `gc` will either return a match if a boolean
-evaluates to true, or `abort`. There are two constructs that are built
-around guarded commands which adds more functionality to them.
-`if gc fi` matches one rule in the guarded statement and executes it. If
-it does not match a rule, it then acts like `abort`. `do gc od` loops
-over the guarded commands while any rule matches. If there no match is
-found, it acts like `skip`.
-
-These allow for nice encoding of common algorithms, using two other
-constructs that use the guarded commands.
-
-{{< /transclude-1 >}}
-
 <div id="refs" class="references csl-bib-body" markdown="1">
 
 <div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
@@ -81,14 +48,6 @@ doi: [10.1145/1111037.1111042].</span>
 
 </div>
 
-<div id="ref-winskel93" class="csl-entry" markdown="1">
-
-<span class="csl-left-margin">\[2\]
-</span><span class="csl-right-inline">G. Winskel, *The formal semantics
-of programming languages: An introduction*. MIT press, 1993.</span>
-
-</div>
-
 </div>
 
   [\#3a]: /zettel/3a
diff --git a/content/zettel/1d1.md b/content/zettel/1d1.md
index dcd131c..cc902c4 100644
--- a/content/zettel/1d1.md
+++ b/content/zettel/1d1.md
@@ -38,6 +38,8 @@ to support a subset of possible recursive functions. Even though these
 are as powerful as loops, it may be more natural to write their
 definitions as a recursive function instead of a loop.
 
+{{< /transclude-1 >}}
+
 {{< transclude-2 zettel="1b1" >}}
 
 Guarded commands \[2\] are an interesting construct which can be added
@@ -71,8 +73,6 @@ constructs that use the guarded commands.
 
 {{< /transclude-2 >}}
 
-{{< /transclude-1 >}}
-
 <div id="refs" class="references csl-bib-body" markdown="1">
 
 <div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
diff --git a/content/zettel/3a8g5h.md b/content/zettel/3a8g5h.md
index 31ab96c..86f9892 100644
--- a/content/zettel/3a8g5h.md
+++ b/content/zettel/3a8g5h.md
@@ -4,7 +4,7 @@ author = "Yann Herklotz"
 tags = []
 categories = []
 backlinks = ["3a8g5g"]
-forwardlinks = ["3a8g5i", "3a8g5h1"]
+forwardlinks = ["3a8g5h1", "3a8g5h2", "4e1", "3a8g5h3", "3a8g5h4", "3a8g5i"]
 zettelid = "3a8g5h"
 +++
 
@@ -31,4 +31,53 @@ independent before the simplification to $1 \lor \neg 1$ and
 $\neg1 \land \neg 2$, where the left hand branch will actually always be
 true.
 
+{{< transclude-1 zettel="3a8g5h1" >}}
+
+The first solution to this problem would be to add quantifiers to the
+atoms that cannot always be evaluated at the current spot. However, this
+would significantly increase the complexity of the Sat solver, as well
+as make predicates unevaluatable in general, because it might contain
+quantifiers that don't evaluate to one specific value.
+
+However, with a suitably strong SAT solver, it should be possible to
+show the independence between the different predicates. However, the
+correctness property should probably be correct as well and should be
+checkable with the SAT solver.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h2" >}}
+
+The second possible solution could be to use Craig interpolation
+([\#4e1]), which was a suggestion by John. This is close to what we
+currently already do, however a bit more sound (replacing positive
+literals by T and replacing negative literals by $\perp$). This does not
+seem to completely solve the problem, because it only really works for
+implication, and for the independence property that's not enough.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h3" >}}
+
+Tri-state logic is also an interesting solution and it goes back to what
+we had initially thought about implementing, however, the problem with
+that is again the SAT solver, as we want to be able to assume that we do
+get an answer out of it. However, maybe it's possible to use the SAT
+solver natively on 3-state logic. We would then be able to construct the
+evaluation rules for our gates so that they follow the correctness
+property that we are hoping for.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h4" >}}
+
+Finally, the fourth solution could be to have lazy evaluation of the
+expressions, and order the predicates so that the more general property
+comes first, followed by the more specific properties. However, the main
+problem with this is that we don't really know which predicate came from
+which node, and what the order should be for those predicates.
+
+{{< /transclude-1 >}}
+
   [1]: attachment:gsa-simplification-problem.png
+  [\#4e1]: /zettel/4e1
diff --git a/content/zettel/3a8g5h2.md b/content/zettel/3a8g5h2.md
index b8facdd..2041559 100644
--- a/content/zettel/3a8g5h2.md
+++ b/content/zettel/3a8g5h2.md
@@ -3,7 +3,7 @@ title = "Second possible solution: Craig interpolation"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h1"]
+backlinks = ["3a8g5h1", "3a8g5h"]
 forwardlinks = ["4e1", "3a8g5h3"]
 zettelid = "3a8g5h2"
 +++
diff --git a/content/zettel/3a8g5h3.md b/content/zettel/3a8g5h3.md
index 73576e5..e521c44 100644
--- a/content/zettel/3a8g5h3.md
+++ b/content/zettel/3a8g5h3.md
@@ -3,7 +3,7 @@ title = "Third possible solution: Tri-state logic"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h2", "3a8g5g1"]
+backlinks = ["3a8g5h2", "3a8g5h", "3a8g5g1"]
 forwardlinks = ["3a8g5h4"]
 zettelid = "3a8g5h3"
 +++
diff --git a/content/zettel/3a8g5h4.md b/content/zettel/3a8g5h4.md
index 9e044b8..e11af4c 100644
--- a/content/zettel/3a8g5h4.md
+++ b/content/zettel/3a8g5h4.md
@@ -3,7 +3,7 @@ title = "Fourth possible solution: Ordering of predicates"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h3"]
+backlinks = ["3a8g5h3", "3a8g5h"]
 forwardlinks = ["3a8g5h5"]
 zettelid = "3a8g5h4"
 +++
diff --git a/content/zettel/4e1.md b/content/zettel/4e1.md
index 71407e9..754204c 100644
--- a/content/zettel/4e1.md
+++ b/content/zettel/4e1.md
@@ -3,7 +3,7 @@ title = "Craig interpolation"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["4e", "3a8g5h2"]
+backlinks = ["4e", "3a8g5h2", "3a8g5h"]
 forwardlinks = ["4e2"]
 zettelid = "4e1"
 +++
diff --git a/layouts/_default/list.html b/layouts/_default/list.html
index 744f390..4cf7dd1 100644
--- a/layouts/_default/list.html
+++ b/layouts/_default/list.html
@@ -6,12 +6,15 @@
 
 {{ .Content }}
 
-<ul>
   {{ $pages := .Pages }}
   {{ if .IsHome }}{{ $pages = .Site.RegularPages }}{{ end }}
-  {{ range (where $pages "Section" "!=" "") }}
+  {{ range $pages.GroupByDate "2006" }}
+  <h2 class="post-year">{{ .Key }}</h2>
+  <table class="post-list">
+  {{ range .Pages }}
   {{ partial "post-element.html" . }}
   {{ end }}
-</ul>
+  </table>
+  {{ end }}
 
 {{ partial "footer.html" . }}
diff --git a/layouts/_default/single.html b/layouts/_default/single.html
index f3953af..e1f98a7 100644
--- a/layouts/_default/single.html
+++ b/layouts/_default/single.html
@@ -1,6 +1,6 @@
 {{ partial "header.html" . }}
 <div class="article-meta">
-<h1><span class="title">{{ .Title | markdownify }}</span></h1>
+<h1><span class="title">{{ .Title | markdownify }}</span>{{ if .Params.zettelid }}<a class="zettel-link" href="{{ .RelPermalink }}"> [#{{ .Params.zettelid }}]</a>{{ end }}</h1>
 <!--{{ with .Params.author }}<h2 class="author">{{ . }}</h2>{{ end }}-->
 {{ if (gt .Params.date 0) }}<h2 class="date">{{ .Date.Format "2006/01/02" }}</h2>{{ end }}
 </div>
@@ -9,22 +9,26 @@
 {{ .Content }}
 </main>
 
-  {{ if (.Page.Param "backlinks") }}
-  <h2>Referenced from</h2>
-  {{ range (.Page.Param "backlinks") }}
-    {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }}
-    {{ partial "post-element.html" . }}
-    {{- end }}
-  {{ end }}
+{{ with (.Page.Param "backlinks") }}
+<h2>Referenced from</h2>
+<table class="post-list">
+{{ range . }}
+  {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }}
+  {{ partial "post-element" . }}
   {{ end }}
+{{ end }}
+</table>
+{{ end }}
 
-  {{ if (.Page.Param "forwardlinks") }}
-  <h2>Links to</h2>
-  {{ range (.Page.Param "forwardlinks") }}
-    {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }}
-    {{ partial "post-element.html" . }}
-    {{- end }}
-  {{ end }}
+{{ with (.Page.Param "forwardlinks") }}
+<h2>Links to</h2>
+<table class="post-list">
+{{ range . }}
+  {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }}
+  {{ partial "post-element" . }}
   {{ end }}
+{{ end }}
+</table>
+{{ end }}
 
 {{ partial "footer.html" . }}
diff --git a/layouts/partials/head_custom.html b/layouts/partials/head_custom.html
index 47ba699..93e3874 100644
--- a/layouts/partials/head_custom.html
+++ b/layouts/partials/head_custom.html
@@ -17,3 +17,4 @@
         });
     });
 </script>
+<link rel="stylesheet" href="{{ "css/custom.css" | relURL }}" />
diff --git a/layouts/partials/post-element.html b/layouts/partials/post-element.html
index b45a1e1..28fff85 100644
--- a/layouts/partials/post-element.html
+++ b/layouts/partials/post-element.html
@@ -1,4 +1,4 @@
-<li>
-  <span class="date">{{ .Date.Format "2006/01/02" }}</span>
-  <a href="{{ .RelPermalink }}">{{ .Title | markdownify }}</a>
-</li>
+<tr>
+  <td>{{ .Title | markdownify }}{{ if .Params.zettelid }}<a class="zettel-link" href="{{ .RelPermalink }}"> [#{{ .Params.zettelid }}]</a>{{ end }}</td>
+  <td class="date-td">{{ with .Date }}<span class="date">{{ .Format "2006/01/02" }}</span>{{ end }}</td>
+</tr>
diff --git a/layouts/shortcodes/transclude-1.html b/layouts/shortcodes/transclude-1.html
index 80a24da..cfc6a86 100644
--- a/layouts/shortcodes/transclude-1.html
+++ b/layouts/shortcodes/transclude-1.html
@@ -1,4 +1,4 @@
 <div class="transclude-1">
-  <h2><a class="transclude-link" href="/zettel/{{ .Get "zettel" }}">{{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}</a></h2>
+  {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}<h2>{{ .Title | markdownify }}<a class="transclude-link" href="{{ .RelPermalink }}"> [#{{ .Params.zettelid }}]</a></h2>{{ end }}
   {{ .Inner | markdownify }}
 </div>
diff --git a/layouts/shortcodes/transclude-2.html b/layouts/shortcodes/transclude-2.html
index a63de87..20987ae 100644
--- a/layouts/shortcodes/transclude-2.html
+++ b/layouts/shortcodes/transclude-2.html
@@ -1,4 +1,4 @@
 <div class="transclude-2">
-  <h3><a class="transclude-link" href="/zettel/{{ .Get "zettel" }}">{{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}</a></h3>
+  {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}<h3>{{ .Title | markdownify }}<a class="transclude-link" href="{{ .RelPermalink }}"> [#{{ .Params.zettelid }}]</a></h3>{{ end }}
   {{ .Inner | markdownify }}
 </div>
diff --git a/layouts/shortcodes/transclude-3.html b/layouts/shortcodes/transclude-3.html
index 1e43c85..6e73cd4 100644
--- a/layouts/shortcodes/transclude-3.html
+++ b/layouts/shortcodes/transclude-3.html
@@ -1,4 +1,4 @@
 <div class="transclude-3">
-  <h4><a class="transclude-link" href="/zettel/{{ .Get "zettel" }}">{{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}</a></h4>
+  {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}<h4>{{ .Title | markdownify }}<a class="transclude-link" href="{{ .RelPermalink }}"> [#{{ .Params.zettelid }}]</a></h4>{{ end }}
   {{ .Inner | markdownify }}
 </div>
diff --git a/themes/hugo-xmin b/themes/hugo-xmin
-Subproject 67f2ed048d0494891a6e9ea8ed2e2bffda43190
+Subproject d29186892211056822e976689c0c6b3eb026f6e