NU-Prolog's and Gödel's logical and sound `if-then-else` extension

A paper about mercury says the following:

The if-then-else and negation constructs in most variants of Prolog are non-logical and unsound: they can cause the system to compute answers which are inconsistent with the program viewed as a logical theory. Some existing logic programming systems such as NU-Prolog and Gödel provide logical and sound replacements for these Prolog constructs. Unfortunately, these systems enforce safety via runtime groundness checks. This effect can increase the runtime of a program by an arbitrarily large factor; if the goals checked for groundness include large terms, the checks can be prohibitively expensive.

NU-Prolog and Gödel look rather dead and non-free, but I still wonder:

What are these logical and sound if-then-else replacements?
Do they have analogs in SWI or GNU Prologs?
How do they work? How could they work? Adding logical negation to Prolog turns it into general FOL, right? You would basically need a general FOL theorem prover to work with it?
Are they different from if_/3? if_/3 has to be extended to be used with new conditions. Would one have to do this in NU-Prolog and Gödel also?

Solution

A break through in if-then-else could be a new annotation. By annotation I understand things like mode declarations, determinancy declarations, etc.. For an if then else, a complete declaration would be nice. Lets assume we could declare a predicate or built-in p/n complete. This would mean it has the property for ground arguments t1,..,tn:

   T |- p(t1,..,tn)

- or -

   T |- ~p(t1,..,tn)

Or in short it would be a decidable predicate if the theory T is recursively enumerable. If we then recall that if-then-else is logically:

    ITE(A,B,C) == (A => B) & (~A => C)

We could then use the complete annotation as follows. Lets assume A = p(t1,..,tn). Because of the annotation the Prolog system would try to prove A. If it doesn't succeed, because of the complete annotation, the Prolog system can infer that ~A would succeed. And therefore it can use the else branch without a proof attempt of ~A.

But interestingly this is already what the ISO core standard if-then-else does, (A->B;C) does also only prove A once. So whats the problem? I guess the problem is that A might be more complex and not necessarily ground. Or even that a predicate p/n might be incomplete, or we even don't know whether it is complete. And in all these cases the ISO core standard nevertheless allows us to use the (A->B;C).

The groundness problem can sometimes be solved by using a runtime groundness checks. This is probably what Mercury refers to:

    when(ground(A), (A->B;C))

SWI-Prolog even applies a trick to make the groundness check cheaper, see also some further discussion on Discourse:

%!  trigger_ground(@Term, :Goal)
%
%   Trigger Goal when Term becomes   ground.  The current implementation
%   uses nonground/2, waiting for an   atribtrary  variable and re-check
%   Term  when  this  variable   is    bound.   Previous   version  used
%   term_variables and suspended  on  a   term  constructed  from  these
%   variables. It is clear  that  either   approach  performs  better on
%   certain types of terms. The term_variables/2  based approach wins on
%   large terms that are almost  ground.   Possibly  we need a nonground
%   that also returns the number of tests   performed  and switch to the
%   term_variables/2 based approach if this becomes large.

trigger_ground(X, Goal) :-
    (   nonground(X, V)
    ->  '$suspend'(V, when, trigger_ground(X, Goal))
    ;   call(Goal)
).