Formalized backtracking - Bjørn Kjos-Hanssen, Bjørn