Proving the impossible is impossible is possible: disproofs based on hereditary partitions
Laurent Siklóssy, J. Roach · International Joint Conference on Artificial Intelligence · 1973
A novel technique, called hereditary partitions, is Introduced. It permits the rigorous proof that, in a given axiomatization, certain states can never be reached. The technique is implemented in a computer program, DISPROVER, and is applied to robot worlds. DISPROVER cooperates with a path-finding program when the latter encounters difficulties.