diff options
Diffstat (limited to 'content/zettel/3c3f3.md')
| -rw-r--r-- | content/zettel/3c3f3.md | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3c3f3.md b/content/zettel/3c3f3.md new file mode 100644 index 0000000..856b100 --- /dev/null +++ b/content/zettel/3c3f3.md @@ -0,0 +1,27 @@ ++++ +title = "Proving that all atoms are evaluable" +date = "2023-02-04" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3f2"] +forwardlinks = ["3c3f4"] +zettelid = "3c3f3" ++++ + +Instead, if one can show that all the atoms of formulas are evaluable, +then one should be able to show that the whole formula will also be +evaluable. Then, one can simply reason about the formulas using binary +logic. This simplifies the solver used to check these predicates, and +reasoning about the predicates in general. + +The main proof-burden of this method is that it requires one proves that +every atom is evaluable, and if one uses a context to evaluate some +predicates, one has to carry around a proof that every predicate in that +context is also evaluable. In addition to that, predicates that could +technically evaluate to a result using short-circuiting will not be +expressible in general in these formulas. For example, a predicate like +the following: `p1 \/ p2`, where `p1` always evaluates to true, and `p2` +might sometimes not be evaluable, is not expressible. This is because in +general one would have to evaluate a predicate `p2` to three possible +values, which would then have to be handled in the `\/` construct. |