CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC

[1] ABRAMSKY S, IN PRESS THEORETICAL

[2] BEESON M, 1991, LNCS, V475, P101

[3] DARDZHANIA GK, 1977, POLISH ACADEMY SCI I, V6, P2

[4] PROVING TERMINATION WITH MULTI-SET ORDERINGS [J]. COMMUNICATIONS OF THE ACM, 1979, 22 (08) : 465 - 476

[5] DERSHOWITZ N, 1979, LNCS, V71, P188

[6] A NOTE ON GENTZENS DECISION PROCEDURE FOR INTUITIONISTIC PROPOSITIONAL LOGIC [J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1987, 33 (05): : 453 - 456

[7] DRAGALIN AD, 1988, T MATH MONOGRAPHS, V67

[8] Dummett M., 1977, ELEMENTS INTUITIONIS

[9] DYCKHOFF R, 1989, COMPUTERISED LOGIC T, V2, P51

[10] FELTY A, 1991, LECT NOTES ARTIF INT, V475, P157

[1] ABRAMSKY S, IN PRESS THEORETICAL

[2] BEESON M, 1991, LNCS, V475, P101

[3] DARDZHANIA GK, 1977, POLISH ACADEMY SCI I, V6, P2

[4] PROVING TERMINATION WITH MULTI-SET ORDERINGS [J]. COMMUNICATIONS OF THE ACM, 1979, 22 (08) : 465 - 476

[5] DERSHOWITZ N, 1979, LNCS, V71, P188

[6] A NOTE ON GENTZENS DECISION PROCEDURE FOR INTUITIONISTIC PROPOSITIONAL LOGIC [J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1987, 33 (05): : 453 - 456

[7] DRAGALIN AD, 1988, T MATH MONOGRAPHS, V67

[8] Dummett M., 1977, ELEMENTS INTUITIONIS

[9] DYCKHOFF R, 1989, COMPUTERISED LOGIC T, V2, P51

[10] FELTY A, 1991, LECT NOTES ARTIF INT, V475, P157