ADDED: not_si/1

[triska]

For a recent example that would benefit from this, see "Prolog Basics Explained with Pokémon" by @alexpetros:

https://unplannedobsolescence.com/blog/prolog-basics-pokemon/

Thank you a lot!

[UWN]

Instantiation error if Goal is not ground.

(And type error if not a term)

[alexpetros]

This is a step in the direction towards completeness, but it still doesn't make not_si monotonic right? Because the objections raised in this thread should still apply?

[UWN]

This is a step in the direction towards completeness, but it still doesn't make not_si monotonic right? Because the objections raised in this thread should still apply?

This was not an objection but an observation. What we have here is called negation as failure (NAF), which means two things: A way to implement this in Prolog (8.15.1 (\+)/1 – not provable) , and an inference rule with its completion semantics.

The simplest way to reconcile both is to use a safe approximation that is correct as long as it terminates and does not produce an error. This is what not_si/1 does. Just like all the other _si predicates. Another way would be to delay execution until the goal is ground, like

 when(ground(G_0),not_si(G_0)).

More elaborate (and much more complex) attempts can be found under the name constructive negation.

All of this remains inherently non-monotonic. This is not a bug. Take as an example the relation child_of/2 and onlychild/1. Now as new children are born and added, some solutions to onlychild/1 no longer hold (and some other solutions may be added monotonically). Thus, there are relations that are inherently non-monotonic (if they are formulated that way).

Quite often, however, (\+)/1 (and its harmless-looking variations (;)/2 – if-then-else and !/0) are used for predicates that should remain pure and monotonic.

Another inherent downside of non-monotonic predicates is that explanations about unexpected success/failure/non-termination/instantiation errors are much more complex (resembling closely the actual execution traces) than in the pure and monotonic subset where we often can reduce the size of the relevant program to a very tiny slice. For this reason focusing on the pure monotonic part first does make a lot of sense.

Another downside of non-monotonic predicates is that they do not fit together easily with constraints whereas the pure monotonic part fits in nicely. This may be resolvable, it is more of an implementation issue, but a very non-trivial one.

[triska]

I now wonder: Should this actually be called not_provable_si/1?

No, apparently not!