Right now we only use the ep check to see whether the goal already occurred above the current step in the proof tree, and we only use it to prune branches of the search tree to prevent infinite loops. Could we instead check if the same goal occurred previously in the search tree and if so just point to the result set of the previous occurrence of the goal? This seems maybe like a kind of memoization optimization and maybe a way to deal with infinite-looping issues for inferencing with existentials
Right now we only use the ep check to see whether the goal already occurred above the current step in the proof tree, and we only use it to prune branches of the search tree to prevent infinite loops. Could we instead check if the same goal occurred previously in the search tree and if so just point to the result set of the previous occurrence of the goal? This seems maybe like a kind of memoization optimization and maybe a way to deal with infinite-looping issues for inferencing with existentials