Feature request: term relevance (through backward-chaining?)

[mengwong]

Traditional web forms distinguish mandatory vs optional fields, to be validated upon form submission. A web form can be thought of as submitting all the fields at once, in a batch.

However, a more general decision logic does not easily admit easy partitioning of ground terms between "mandatory" and "optional".

In a UI which allows the end user to more interactively fill in values for input fields – "valuating ground terms incrementally" – a reasoner should be able to determine, upon each field input, which fields to ask for next, without obsessing over the mandatory/optional distinction.

red == 1 and (green > 0 or blue == 42)

Most people would consider that red is mandatory … at first … or at least relevant. Let's see.

If red = 2 then green and blue are optional – no longer relevant – because we short circuit to answer=False.

If red = 1 then green and blue are relevant though neither is strictly mandatory

Because if green is -100 then blue becomes mandatory

But if green is 100 then blue is optional

If the user fills in blue = 42 then we don't need to ask for green

So in this case the UI should operate in three steps

1. Red: [__]  Green: [__]   Blue: [__]

User gives red = 1

2. Green: [__]   Blue: [__]

User gives blue = 40

3. Green: [__]

User gives green = 100

Answer: true

Why isn't red a mandatory field? Because if both green and blue resolve to negative then we don't need red any more to return false.

[mengwong]

We can compose this problem with the related problem of allowing end users to answer parent nodes. "I know that the green/blue sub expression is true, but for privacy reasons I cannot tell you which of green or blue satisfies"

[ym-han]

As a quick note, YScript seems to do something like the first feature request, and they seem to do it using Z3: https://wohanley.com/posts/visual-yscript/#explanation