We prove strong normalization of tq-reduction for all standard versions of sequent calculus for classical and intuitionistic (second and first order) logic and give a perspicuous argument for the completeness of the focusing restriction on sequent derivations.
CITATION STYLE
Joinet, J. B., Schellinx, H., & De Falco, L. T. (1996). Strong normalization for all-style LKtq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1071, pp. 226–243). Springer Verlag. https://doi.org/10.1007/3-540-61208-4_15
Mendeley helps you to discover research relevant for your work.