If I have that EGT which is faulty as described by me above, but I don't know it in advance, I read the claim that the given position is "mate in 3" while in reality it is "mate in 2". So the first proof tree is built to prove the "mate in at most 3" and it does not fail. If I understand you correctly the second proof tree would be built in order to prove that none of the other moves for the winning side results in a faster mate, right? So you try all white moves, including 1.Qg2. The latter will result in a mate in 2 so we are done, EGT fault detected. But the algorithm implies to also check all other non-optimal moves which is a lot of work.syzygy wrote:Ok, but I had already written that the proof tree for proving "mate in at most N" will not work for proving that the position is not mate in less than N. ("Again, this does not prove that no shorter mate exists.")Sven Schüle wrote:The claim of a mate in 3 would be "confirmed" although it is wrong.
For that, you need to work the other way around. Find for every move by the winning side one countermove that sufficiently delays the mate (or even draws or wins the game). Same principle.
You can also do both at once, very much like how a principal variation search works. The PV will be what joins the two trees.
I think I now understand how the proof tree building works from your viewpoint. How do you handle the effort resulting from trying all non-optimal moves for the winning side?