Strong Normalization for All-Style LK tq Extended Abstract
We prove strong normalization of tq-reduction for all standard versions of sequent calculus for classical and intuitionistic (second and rst order) logic and give a perspicuous argument for the completeness of the focusing restriction on sequent derivations.