blob: 856b1003f95d1b7f02cfd773ed97c3f94b2680aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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.
|
