The Admitted Shortcut: Tree search over sub-specifications of a decidable logic — shortcuts under a decided, bound admission record, controlled change of the tables they read, and a forward shortcut with a decided margin, with Tau Chess as the worked example

A search program saves work by shortcuts that stop a loop over candidates, or skip a candidate, where the choice cannot change. In the method described here the work of a search is spread over small sub-specifications of a logic with a decision procedure, and a shortcut acts only if a statement about its executed text, decided for all assignments of its inputs, is bound to that text by its hash in an admission record; otherwise the condition that reads it has no effect, and the loop runs on without the shortcut (the fallback rule). For shortcuts that only save work, a missing or unfitting admission costs evaluations, not the choice. The same record governs the change of a table a shortcut reads, taken over only when the shortcut's precondition is decided for the new text, and a forward shortcut whose margin is decided over the executed scoring. Around this core the paper describes the exchange of an executed text for a reformulated one of decided equality, the binding of records to the build of the evaluation unit, a search of fixed depth from a number, a depth chosen per phase by a sub-specification, and workers whose merge and shared bound are outputs of an admitted sub-specification. The worked example is Tau Chess, built from sub-specifications of the Tau language, created by Ohad Asor and developed by IDNI AG. Run on builds of its evaluation unit are the search with admission records, a start check that refuses and names the reason, a fallback with the same moves at more calls, the exchange of 19 executed texts, a search of fixed depth with workers call for call equal to a reference model, a game with depth per phase ending in mate, the reopening of an execution unit after an unexpected end, and a learning cycle in which a table proposed from the program's own games is taken over only after the precondition of the reading shortcuts is decided over its text. The forward shortcut exists in a smallest form only. One game against a language model and series of games against a chess program are reported; nothing here is a statement about playing strength. ---