zlacker

Thanks for confirming this. With your reply in mind I think there is no reasonable way to make BFS the default for a logic language, and the programmer will just have to choose between BFS and DFS.

In other words, the answer to TFA's title question is, I think, "no" as to backtracking/DFS.

>>crypto+(OP)
To be honest I'd like it to be possible to completely do away with graph search in Resolution-based theorem proving. Resolution itself assumes no search, it's only an inference rule that removes contradictions from a theory. The original paper on Resolution proposes various ways to implement it but they all come down to search of some sort. I guess that's all we know how to do in AI: search :/