Lambda the Ultimate

I have been struggling with negation in logic programming for a while. There is a fundamental problem with negation because failure to find a proof is not the same thing as a disproof. This makes the common 'negation as failure' approach unsound.

I have looked at many alternatives, like negation as inconsistency, and 3 or 4 valued logics, and whilst some of these have merit they make both the language and the implementation much more complicated. This makes logic programming lose some of its elegance.

I considered for a while that negation was unnecessary, but that results in redundant code for simple examples like 'member' and 'not member'.

I think the fundamental problem is the confusion between the 'proof' and a boolean.

x.
:- x.
true.

Is misleading because we have proved 'x', but not really 'x true'. Let's instead write:

x.
:- x.
proved.

So we want to encode that x is true, we should rather write:

(x, true)
:- (x, X).
X = true, proved.

In this way we can write member, and negation of a boolean, in simple Horn clause logic, with only the addition of an disequality constraint, so that the order of clause execution is not significant:

not(true, false).
not(false, true).

member(X, cons(X, Tail), true).
member(X, nil, false).
member(X, cons(Y, Tail), Result) :-
    dif(X, Y),
    member(X, Tail, Result).

not_member(X, List, Result) :-
    member(X, List, IsMember),
    not(IsMember, Result).

This style is of course not as neat or easy to read as the default way that 'not' is used. The problem appears to be the confusion between the program as a proof and the return value. That a something is proved or not-proved is not the same thing as a function return value at all. So what if we instead treat 'failure' as an exception. We would then return a value from the Prolog clause like a function. We could instead write:

not(true) -> false.
not(false) -> true.

member(X, cons(X, Tail)) -> true.
member(X, nil) -> false.
member(X, cons(Y, Tail)) -> dif(X, Y), member(X, Tail).

not_member(X, List) -> not(member(X, List)).

Hopefully it is obvious what is going on here. I have adopted a different symbol (-> instead of :-) to reinforce that we are returning a value not the success/failure of the program. This keeps the language implementation simple, and avoids the whole negation of proofs problem. I would argue that disproofs are impossible, you can only prove something false, hence the idea of a negation of a proof is meaningless. With failure as an exception we keep the nice syntax of negation in logic programs, but also gain the ability to return more than true/false, moving the logic language a little bit towards functional programming.

Questions:

What do you think of this approach?

I haven't been able to find anything like this approach looking for 'failure as an exception', has this been looked at under a different name, or is there any literature already out there about a similar concept?

Edit: To clarify my use of the term failure as an exception, I mean that unlike Prolog where a clause can evaluate true or false, failure is not returned at all, however it does still trigger backtracking. The change is mostly syntactic sugar for horn clause logic with an 'out' mode final argument.

Edit2: changed "/=" to "dif" to match the usage in Prolog.