I wrote this simple Prolog program.
man(socrates).
mortal(X) :- man(X).
immortal(X) :- immortal(X).
I asked it the usual questions, such as whether Socrates is a man or if Socrates is a mortal.
?- man(socrates).
true. //we know for a fact that Socrates is a man
?- mortal(socrates).
true. //and it can logically be inferred that Socrates is mortal
?- immortal(socrates).
//but we can't seem to figure out if he's immortal
It crashed because of the recursive definition of immortal
. Circular references also make it crash or error with Out of stack space.
It seems to me that, at least in this case, it would be fairly trivial for Mr. Prolog to conclude that from the rules in the program, it cannot be inferred that Socrates is immortal. How? I imagine it could examine the stack and see if it is traversing a rule that has already been traversed.
Is there a reason why this isn't already implemented? Would there be some problem with doing so that I am overlooking, or are there implementations of Prolog that already perform such analysis?