no. R3
Complexity of theorem-proving procedures : some general properties
Revue française d'automatique informatique recherche opérationnelle. Informatique théorique, Tome 8 (1974) no. R3, pp. 5-18. 
@article{ITA_1974__8_3_5_0,
     author = {Longo, G. and Venturini Zilli, M.},
     title = {Complexity of theorem-proving procedures : some general properties},
     journal = {Revue fran\c{c}aise d'automatique informatique recherche op\'erationnelle. Informatique th\'eorique},
     pages = {5--18},
     publisher = {Dunod-Gauthier-Villars},
     address = {Paris},
     volume = {8},
     number = {R3},
     year = {1974},
     mrnumber = {375834},
     zbl = {0302.68098},
     language = {en},
     url = {http://archive.numdam.org/item/ITA_1974__8_3_5_0/}
}
TY  - JOUR
AU  - Longo, G.
AU  - Venturini Zilli, M.
TI  - Complexity of theorem-proving procedures : some general properties
JO  - Revue française d'automatique informatique recherche opérationnelle. Informatique théorique
PY  - 1974
SP  - 5
EP  - 18
VL  - 8
IS  - R3
PB  - Dunod-Gauthier-Villars
PP  - Paris
UR  - http://archive.numdam.org/item/ITA_1974__8_3_5_0/
LA  - en
ID  - ITA_1974__8_3_5_0
ER  - 
%0 Journal Article
%A Longo, G.
%A Venturini Zilli, M.
%T Complexity of theorem-proving procedures : some general properties
%J Revue française d'automatique informatique recherche opérationnelle. Informatique théorique
%D 1974
%P 5-18
%V 8
%N R3
%I Dunod-Gauthier-Villars
%C Paris
%U http://archive.numdam.org/item/ITA_1974__8_3_5_0/
%G en
%F ITA_1974__8_3_5_0
Longo, G.; Venturini Zilli, M. Complexity of theorem-proving procedures : some general properties. Revue française d'automatique informatique recherche opérationnelle. Informatique théorique, Tome 8 (1974) no. R3, pp. 5-18. http://archive.numdam.org/item/ITA_1974__8_3_5_0/

[1] Ausiello G., Complexity hounded universal fonctions, Conference Record of the International Symposium on Theory of machines and Computations, Haifa, 1971.

[2] Blum M., A machine independent theory of complexity of recursive fonction, JACM 14, 1967, pp. 322-336. | MR | Zbl

[3], Bundy A. There is no best proof procedure, ACM SIGART Newsletter, Dec. 1971, pp. 6-7.

[4]Cook S. A., The complexity of theorem-proving procedures, III Annual Symposium on Theory of computation, Ohio, 1971, pp. 151-158. | Zbl

[5] Hartmanis J. and Hopcroft J., An overview of the theory of computational complexity, JACM 18, 1971, pp. 444-475. | MR | Zbl

[6] Kowalski R. and Kuehner D., Linear resolution with selection fonction, Artificial Intelligence 2, 1971, pp. 227-260. | MR | Zbl

[7] Lynch N., Recursive approximation to the halting problem, Rep. of the Tufts University, Medford, Masss., Jan. 1973, pp. 15.

[8] Meltzer B., Prolegomena to a Theory of efficiency of proof procedures, in ArtificialIntelligence and Heuristic programs, American Elzevier, 1971, pp. 15-33.

[9] Meyer A. R., An open problem on creative sets, SIGACT News, April 1973, pp. 20.

[10] Rabin M. O., Degrees of difficulty of Computing a fonction and a partial ordering of recursive sets, Tech, report n. 2, Jerusalem, 1960, pp. 18.

[11] Rogers H., Theory of recursive functions and effective computability, McGraw Hill, 1967, pp. 472. | MR | Zbl