Geodesic
Statistical methods for comparing theorem proving algorithms
Kybernetika, Tome 10 (1974) no. 3, pp. 221-240 Cet article a éte moissonné depuis la source Czech Digital Mathematics Library

Voir la notice de l'article

Classification : 68A40, 68T15 
@article{KYB_1974_10_3_a3,
     author = {Kramosil, Ivan and Zwinogrodzki, Zbigniew},
     title = {Statistical methods for comparing theorem proving algorithms},
     journal = {Kybernetika},
     pages = {221--240},
     year = {1974},
     volume = {10},
     number = {3},
     mrnumber = {0345460},
     zbl = {0284.68068},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/KYB_1974_10_3_a3/}
}
TY  - JOUR
AU  - Kramosil, Ivan
AU  - Zwinogrodzki, Zbigniew
TI  - Statistical methods for comparing theorem proving algorithms
JO  - Kybernetika
PY  - 1974
SP  - 221
EP  - 240
VL  - 10
IS  - 3
UR  - http://geodesic.mathdoc.fr/item/KYB_1974_10_3_a3/
LA  - en
ID  - KYB_1974_10_3_a3
ER  - 
%0 Journal Article
%A Kramosil, Ivan
%A Zwinogrodzki, Zbigniew
%T Statistical methods for comparing theorem proving algorithms
%J Kybernetika
%D 1974
%P 221-240
%V 10
%N 3
%U http://geodesic.mathdoc.fr/item/KYB_1974_10_3_a3/
%G en
%F KYB_1974_10_3_a3
Kramosil, Ivan; Zwinogrodzki, Zbigniew. Statistical methods for comparing theorem proving algorithms. Kybernetika, Tome 10 (1974) no. 3, pp. 221-240. http://geodesic.mathdoc.fr/item/KYB_1974_10_3_a3/

[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

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

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

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

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

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

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

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

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

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

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

[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

[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

[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

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

[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

[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

[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

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

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

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