§3.1 Introducing BCK Games (with reversible backtracking).
A language L for Arithmetic. The judgement tree.
Eloise and Abelard, conjunctive and disjunctive judgements.
Backtracking Games (with reversible backtracking).
A generic position of the play in tree form.
A generic position of the play in sequent form.
Created by Mathematica (October 20, 2006)