Is it possible to write an inconsistent Prolog program using only pure Prolog, cut and `false`?

Question

This one tickled my interest in theory:

Is it possible to write an inconsistent Prolog program, i.e. a program that answers both false and true depending on how it is queried, using only pure Prolog, the cut, and false?

For example, one could query p(1) and the Prolog Processor would says false. But when one queries p(X) the Prolog Processor would give the set of answers 1, 2, 3.

This can be easily achieved with "computational state examination predicates" like var/1 (really better called fresh/1) + el cut:

p(X) :- nonvar(X),!,member(X,[2,3]).
p(X) :- member(X,[1,2,3]).

Then

?- p(1).
false.

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

"Ouch time" ensues if this is high-assurance software. Naturally, any imperative program has no problem going off the rails like this on every other line.

So. can be done without those "computational state examination predicates"?

P.S.

The above illustrates that all the predicates of Prolog are really carrying a threaded hidden argument of the "computational state":

p(X,StateIn,StateOut).

which can be used to explain the behavour of var/1 and friends. The Prolog program is then "pure" when it only calls predicates that neither consult not modify that State. Well, at least that seems to be a good way to look at what is going on. I think.

Answer 1

Here's a very simple one:

f(X,X) :- !, false.
f(0,1).

Then:

| ?- f(0,1).

yes
| ?- f(X,1).

no
| ?- f(0,Y).

no

So Prolog claims there are no solutions to the queries with variables, although f(0,1) is true and would be a solution to both.

Answer 2

Here is one attempt. The basic idea is that X is a variable iff it can be unified with both a and b. But of course we can't write this as X = a, X = b. So we need a "unifiable" test that succeeds without binding variables like =/2 does.

First, we need to define negation ourselves, since it's impure:

my_not(Goal) :-
    call(Goal),
    !,
    false.
my_not(_Goal).

This is only acceptable if your notion of pure Prolog includes call/1. Let's say that it does :-)

Now we can check for unifiability by using =/2 and the "not not" pattern to preserve success while undoing bindings:

unifiable(X, Y) :-
    my_not(my_not(X = Y)).

Now we have the tools to define var/nonvar checks:

my_var(X) :-
    unifiable(X, a),
    unifiable(X, b).

my_nonvar(X) :-
    not(my_var(X)).

Let's check this:

?- my_var(X).
true.

?- my_var(1).
false.

?- my_var(a).
false.

?- my_var(f(X)).
false.

?- my_nonvar(X).
false.

?- my_nonvar(1).
true.

?- my_nonvar(a).
true.

?- my_nonvar(f(X)).
true.

The rest is just your definition:

p(X) :-
    my_nonvar(X),
    !,
    member(X, [2, 3]).
p(X) :-
    member(X, [1, 2, 3]).

Which gives:

?- p(X).
X = 1 ;
X = 2 ;
X = 3.

?- p(1).
false.

Edit: The use of call/1 is not essential, and it's interesting to write out the solution without it:

not_unifiable(X, Y) :-
    X = Y,
    !,
    false.
not_unifiable(_X, _Y).

unifiable(X, Y) :-
    not_unifiable(X, Y),
    !,
    false.
unifiable(_X, _Y).

Look at those second clauses of each of these predicates. They are the same! Reading these clauses declaratively, any two terms are not unifiable, but also any two terms are unifiable! Of course you cannot read these clauses declaratively because of the cut. But I find this especially striking as an illustration of how catastrophically impure the cut is.