Complexity of theorem-proving procedures : some general properties
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 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 = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {5--18},
publisher = {Dunod-Gauthier-Villars},
address = {Paris},
volume = {8},
number = {R3},
year = {1974},
zbl = {0302.68098},
mrnumber = {375834},
language = {en},
url = {http://www.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  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 1974
DA  - 1974///
SP  - 5
EP  - 18
VL  - 8
IS  - R3
PB  - Dunod-Gauthier-Villars
PP  - Paris
UR  - http://www.numdam.org/item/ITA_1974__8_3_5_0/
UR  - https://zbmath.org/?q=an%3A0302.68098
UR  - https://www.ams.org/mathscinet-getitem?mr=375834
LA  - en
ID  - ITA_1974__8_3_5_0
ER  - 
Longo, G.; Venturini Zilli, M. Complexity of theorem-proving procedures : some general properties. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 8 (1974) no. R3, pp. 5-18. http://www.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 235912 | Zbl 0155.01503

[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 0253.68020

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

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

[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 224462 | Zbl 0183.01401