PROOF NORMALIZATION FOR RESOLUTION AND PARAMODULATION

[1] [Anonymous], SYMBOLIC LOGIC MECHA

[2] Bachmair L., 1986, Proceedings of the Symposium on Logic in Computer Science (Cat. No.86CH2321-8), P346

[3] BACHMAIR L, 1987, THESIS U ILLINOIS UR

[4] Brand D., 1975, SIAM Journal on Computing, V4, P412, DOI 10.1137/0204036

[5] BROWN T, 1975, THESIS CALTECH PASAD

[6] ORDERINGS FOR TERM-REWRITING SYSTEMS [J]. THEORETICAL COMPUTER SCIENCE, 1982, 17 (03) : 279 - 301

[7] TERMINATION OF REWRITING [J]. JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) : 69 - 116

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

[9] GANZINGER H, 1988, IN PRESS J SYMBOLIC

[10] HSIANG J, 1986, LECT NOTES COMPUT SC, V230, P141

[1] [Anonymous], SYMBOLIC LOGIC MECHA

[2] Bachmair L., 1986, Proceedings of the Symposium on Logic in Computer Science (Cat. No.86CH2321-8), P346

[3] BACHMAIR L, 1987, THESIS U ILLINOIS UR

[4] Brand D., 1975, SIAM Journal on Computing, V4, P412, DOI 10.1137/0204036

[5] BROWN T, 1975, THESIS CALTECH PASAD

[6] ORDERINGS FOR TERM-REWRITING SYSTEMS [J]. THEORETICAL COMPUTER SCIENCE, 1982, 17 (03) : 279 - 301

[7] TERMINATION OF REWRITING [J]. JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) : 69 - 116

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

[9] GANZINGER H, 1988, IN PRESS J SYMBOLIC

[10] HSIANG J, 1986, LECT NOTES COMPUT SC, V230, P141