HARD EXAMPLES FOR RESOLUTION

[1] A SIMPLIFIED PROOF THAT REGULAR RESOLUTION IS EXPONENTIAL [J]. INFORMATION PROCESSING LETTERS, 1980, 10 (02) : 96 - 98

[2] BLAKE A, 1938, J SYMBOLIC LOGIC, V3, P93

[3] Church, 1956, INTRO MATH LOGIC, V1

[4] COOK S, 1976, ACM SIGACT NEWS, V8, P28

[5] RELATIVE EFFICIENCY OF PROPOSITIONAL PROOF SYSTEMS [J]. JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (01) : 36 - 50

[6] Gabber O., 1979, 20th Annual Symposium of Foundations of Computer Science, P364, DOI 10.1109/SFCS.1979.16

[7] Galil Z., 1977, SIAM Journal on Computing, V6, P444, DOI 10.1137/0206031

[8] Galil Z., 1977, Theoretical Computer Science, V4, P23, DOI 10.1016/0304-3975(77)90054-8

[9] THE INTRACTABILITY OF RESOLUTION [J]. THEORETICAL COMPUTER SCIENCE, 1985, 39 (2-3) : 297 - 308

[10] Johnson NL, 1970, DISCRETE DISTRIBUTIO

[1] A SIMPLIFIED PROOF THAT REGULAR RESOLUTION IS EXPONENTIAL [J]. INFORMATION PROCESSING LETTERS, 1980, 10 (02) : 96 - 98

[2] BLAKE A, 1938, J SYMBOLIC LOGIC, V3, P93

[3] Church, 1956, INTRO MATH LOGIC, V1

[4] COOK S, 1976, ACM SIGACT NEWS, V8, P28

[5] RELATIVE EFFICIENCY OF PROPOSITIONAL PROOF SYSTEMS [J]. JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (01) : 36 - 50

[6] Gabber O., 1979, 20th Annual Symposium of Foundations of Computer Science, P364, DOI 10.1109/SFCS.1979.16

[7] Galil Z., 1977, SIAM Journal on Computing, V6, P444, DOI 10.1137/0206031

[8] Galil Z., 1977, Theoretical Computer Science, V4, P23, DOI 10.1016/0304-3975(77)90054-8

[9] THE INTRACTABILITY OF RESOLUTION [J]. THEORETICAL COMPUTER SCIENCE, 1985, 39 (2-3) : 297 - 308

[10] Johnson NL, 1970, DISCRETE DISTRIBUTIO