[1] A. Špaček: Statistical Estimation of Probability in Boolean Logics. In: Transactions of the Second Prague Conference on Information Theory. Prague 1960, 609-626. MR 0123477

[2] A. Špaček: Statistical Estimation of Semantic Probability. In: Proceedings of the fifth Berkeley Symposium on Mathematical Statistics, 1960, vol. 1, 655-688.

[3] I. Kramosil: Statistical Estimation of Deducibility in Polyadic Algebras. Kybernetika 7 (1971), 3, 181-200. MR 0300881 | Zbl 0216.29502

[4] I. Kramosil: A Method for Random Sampling of Well-Formed Formulas. Kybernetika 8 (1972), 2, 133-148. MR 0343414 | Zbl 0242.02014

[5] A. Chirch: A note on the Entscheidungsproblem. The Journal of Symbolic Logic 1, (1936), 40-41.

[6] J. A. Robinson: Theorem-proving on the Computer. Journal of the Assoc. for Comput. Mach. 10 (1963), 163-174. MR 0149693 | Zbl 0109.35603

[7] H. Wang: Toward Mechanical Mathematics. IBM J. Res. Develop. 4 (1960), 2-22. MR 0113291 | Zbl 0106.00802

[8] Gentzen G.: Untersuchungen über das logische Schliessen. Math. Zeit. 39 (1934-35), 176-210. Zbl 0010.14601

[9] W. Craig: Linear Reasoning - a New Form of Herbrand - Gentzen Theorem. The Journal of Symboic Logic 22 (1957), 250-268. MR 0104564

[10] Beth E. W.: Formal Methods. D. Reidel Publishing Company, Dordrecht, 1962. MR 0160709 | Zbl 0105.24503

[11] S. W. Szczerba: Semantic Method of Proving Theorems. Bull. de ľAcademie Polonaise des Sciences. Serie des sciences math., astr. et phys. 18 (1970), 9, 507-512. MR 0274257 | Zbl 0212.03003

[12] J. A. Robinson: A Machine Oriented Logic Based on the Resolution Principle. J. Assoc. Comput. Mach. 12 (1965), 23-41. MR 0170494 | Zbl 0139.12303

[1З] J. A. Robinson: The Generalized Resolution Principle. Machine Intelligence 3, Edinburgh University Press, 1968, 77-93. Zbl 0195.31102

[14] S. Ju. Masłov: The Inverse Method for Establishing Deducibility for Logical Calculi. Trudy Matem. Inst. Steklov. Translation: Proc. Steklov Inst. Math. 98, (1968), 26-87. MR 0252195

[15] Maslov S. Ju.: An Inverse Method of Establishing Deducibility of Non-prenex Formulas of the Predicate Calculus. Translation: Soviet Math. Dokl. 8 (1967), 1, 16-19. MR 0209115

[16] R. Kowalski: An Exposition of Paramodulation with Refinements. Department of Computational Logic, University of Edinburgh, 1968.

[17] J. A. Robinson S. Wos: Paramodulation and Theorem-Proving in First-Order Theories with Equality. Machine Intelligence 4 (1969), Edinburgh Uпiversity Press, 135-150. MR 0275720

[18] S. C. van Westrhenen: Statistical Studies of Theoremhood in Classical Propositional and First-Order Predicate Calculus. J. Assoc. Comp. Mach. 19 (1972), 2, 347-365. MR 0297524 | Zbl 0246.68017

[19] S. Ju. Masłov E. D. Rusakov: Probabilistic Canonical Systems. Translation: Seminars in Mathematics V. A. Steklov Math. Inst., Leningrad, 32 (1972), 66-76. MR 0344089

[20] B. A. Trachtenbrot: Složnosť algoritmov i vyčislenij. Novosibirsk 1967.

[21] G. S. Tseitin: On the complexity of Derivation in Propositional Calculus. Seminars in Mathematics V. A. Steklov Math. Inst., Leningrad, 8 (1970), 115-125.

[22] S. Ju. Masłov: Relationship Between Tactics of the Inverse Method and the Resolution Method. Ibid, 16 (1971), 69-73.

[23] D. G. Kuehner D. G.: A Note on the Relation Between Resolution and Masłov's Inverse Method. Machine Intelligence 6, Edinburgh University Press, 1971, 73-76. Zbl 0263.68049

[24] Orłowska E.: Theorem-proving systems. Dissertationes Mathematicae. PWN, Warszawa 1973.

[25] M. Loève: Probability Theory. Second Edition. D. van Nostrand Comp., Princeton, New Jersey-Toronto-New York-London 1961. MR 0123342

[26] B. V. Gnedenko: Kurs teoriji verojatnostej. Third Edition, Firmatgiz, Moskva 1961.

[27] A. Walde: Sequential Analysis. Russian Translation: Fizmatgiz, Moskva 1960. MR 0116440

[28] E. L. Lehman: Statistical Hypotheses Testing. Russian Translation. Nauka, Moskva 1964.