| Title:
|
Statistical methods for comparing theorem proving algorithms (English) |
| Author:
|
Kramosil, Ivan |
| Author:
|
Zwinogrodzki, Zbigniew |
| Language:
|
English |
| Journal:
|
Kybernetika |
| ISSN:
|
0023-5954 |
| Volume:
|
10 |
| Issue:
|
3 |
| Year:
|
1974 |
| Pages:
|
(221)-240 |
| . |
| Category:
|
math |
| . |
| MSC:
|
68A40 |
| MSC:
|
68T15 |
| idZBL:
|
Zbl 0284.68068 |
| idMR:
|
MR0345460 |
| . |
| Date available:
|
2009-09-24T16:39:32Z |
| Last updated:
|
2012-06-05 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/124528 |
| . |
| Reference:
|
[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 |
| Reference:
|
[2] A. Špaček: Statistical Estimation of Semantic Probability.In: Proceedings of the fifth Berkeley Symposium on Mathematical Statistics, 1960, vol. 1, 655-688. |
| Reference:
|
[3] I. Kramosil: Statistical Estimation of Deducibility in Polyadic Algebras.Kybernetika 7 (1971), 3, 181-200. Zbl 0216.29502, MR 0300881 |
| Reference:
|
[4] I. Kramosil: A Method for Random Sampling of Well-Formed Formulas.Kybernetika 8 (1972), 2, 133-148. Zbl 0242.02014, MR 0343414 |
| Reference:
|
[5] A. Chirch: A note on the Entscheidungsproblem.The Journal of Symbolic Logic 1, (1936), 40-41. |
| Reference:
|
[6] J. A. Robinson: Theorem-proving on the Computer.Journal of the Assoc. for Comput. Mach. 10 (1963), 163-174. Zbl 0109.35603, MR 0149693 |
| Reference:
|
[7] H. Wang: Toward Mechanical Mathematics.IBM J. Res. Develop. 4 (1960), 2-22. Zbl 0106.00802, MR 0113291 |
| Reference:
|
[8] Gentzen G.: Untersuchungen über das logische Schliessen.Math. Zeit. 39 (1934-35), 176-210. Zbl 0010.14601 |
| Reference:
|
[9] W. Craig: Linear Reasoning - a New Form of Herbrand - Gentzen Theorem.The Journal of Symboic Logic 22 (1957), 250-268. MR 0104564 |
| Reference:
|
[10] Beth E. W.: Formal Methods.D. Reidel Publishing Company, Dordrecht, 1962. Zbl 0105.24503, MR 0160709 |
| Reference:
|
[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. Zbl 0212.03003, MR 0274257 |
| Reference:
|
[12] J. A. Robinson: A Machine Oriented Logic Based on the Resolution Principle.J. Assoc. Comput. Mach. 12 (1965), 23-41. Zbl 0139.12303, MR 0170494 |
| Reference:
|
[1З] J. A. Robinson: The Generalized Resolution Principle.Machine Intelligence 3, Edinburgh University Press, 1968, 77-93. Zbl 0195.31102 |
| Reference:
|
[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 |
| Reference:
|
[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 |
| Reference:
|
[16] R. Kowalski: An Exposition of Paramodulation with Refinements.Department of Computational Logic, University of Edinburgh, 1968. |
| Reference:
|
[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 |
| Reference:
|
[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. Zbl 0246.68017, MR 0297524 |
| Reference:
|
[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 |
| Reference:
|
[20] B. A. Trachtenbrot: Složnosť algoritmov i vyčislenij.Novosibirsk 1967. |
| Reference:
|
[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. |
| Reference:
|
[22] S. Ju. Masłov: Relationship Between Tactics of the Inverse Method and the Resolution Method.Ibid, 16 (1971), 69-73. |
| Reference:
|
[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 |
| Reference:
|
[24] Orłowska E.: Theorem-proving systems.Dissertationes Mathematicae. PWN, Warszawa 1973. |
| Reference:
|
[25] M. Loève: Probability Theory.Second Edition. D. van Nostrand Comp., Princeton, New Jersey-Toronto-New York-London 1961. MR 0123342 |
| Reference:
|
[26] B. V. Gnedenko: Kurs teoriji verojatnostej.Third Edition, Firmatgiz, Moskva 1961. |
| Reference:
|
[27] A. Walde: Sequential Analysis.Russian Translation: Fizmatgiz, Moskva 1960. MR 0116440 |
| Reference:
|
[28] E. L. Lehman: Statistical Hypotheses Testing.Russian Translation. Nauka, Moskva 1964. |
| . |
