Add content

1 files changed, 20 insertions, 0 deletions

diff --git a/content/zettel/3a8g5h1.md b/content/zettel/3a8g5h1.md
new file mode 100644
index 0000000..cf3c1cf
--- /dev/null
+++ b/content/zettel/3a8g5h1.md
@@ -0,0 +1,20 @@
++++
+title = "First possible solution: Quantifiers"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5h"]
+forwardlinks = ["3a8g5h2"]
+zettelid = "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.