Statistical methods for comparing theorem proving algorithms

Ivan Kramosil; Zbigniew Zwinogrodzki

Kybernetika (1974)

  • Volume: 10, Issue: 3, page (221)-240
  • ISSN: 0023-5954

How to cite

top

Kramosil, Ivan, and Zwinogrodzki, Zbigniew. "Statistical methods for comparing theorem proving algorithms." Kybernetika 10.3 (1974): (221)-240. <http://eudml.org/doc/27683>.

@article{Kramosil1974,
author = {Kramosil, Ivan, Zwinogrodzki, Zbigniew},
journal = {Kybernetika},
language = {eng},
number = {3},
pages = {(221)-240},
publisher = {Institute of Information Theory and Automation AS CR},
title = {Statistical methods for comparing theorem proving algorithms},
url = {http://eudml.org/doc/27683},
volume = {10},
year = {1974},
}

TY - JOUR
AU - Kramosil, Ivan
AU - Zwinogrodzki, Zbigniew
TI - Statistical methods for comparing theorem proving algorithms
JO - Kybernetika
PY - 1974
PB - Institute of Information Theory and Automation AS CR
VL - 10
IS - 3
SP - (221)
EP - 240
LA - eng
UR - http://eudml.org/doc/27683
ER -

References

top
  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. (1960) MR0123477
  2. A. Špaček, Statistical Estimation of Semantic Probability, In: Proceedings of the fifth Berkeley Symposium on Mathematical Statistics, 1960, vol. 1, 655-688. (1960) 
  3. I. Kramosil, Statistical Estimation of Deducibility in Polyadic Algebras, Kybernetika 7 (1971), 3, 181-200. (1971) Zbl0216.29502MR0300881
  4. I. Kramosil, A Method for Random Sampling of Well-Formed Formulas, Kybernetika 8 (1972), 2, 133-148. (1972) Zbl0242.02014MR0343414
  5. A. Chirch, A note on the Entscheidungsproblem, The Journal of Symbolic Logic 1, (1936), 40-41. (1936) 
  6. J. A. Robinson, Theorem-proving on the Computer, Journal of the Assoc. for Comput. Mach. 10 (1963), 163-174. (1963) Zbl0109.35603MR0149693
  7. H. Wang, Toward Mechanical Mathematics, IBM J. Res. Develop. 4 (1960), 2-22. (1960) Zbl0106.00802MR0113291
  8. Gentzen G., Untersuchungen über das logische Schliessen, Math. Zeit. 39 (1934-35), 176-210. (1934) Zbl0010.14601
  9. W. Craig, Linear Reasoning - a New Form of Herbrand - Gentzen Theorem, The Journal of Symboic Logic 22 (1957), 250-268. (1957) MR0104564
  10. Beth E. W., Formal Methods, D. Reidel Publishing Company, Dordrecht, 1962. (1962) Zbl0105.24503MR0160709
  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. (1970) Zbl0212.03003MR0274257
  12. J. A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, J. Assoc. Comput. Mach. 12 (1965), 23-41. (1965) Zbl0139.12303MR0170494
  13. J. A. Robinson, The Generalized Resolution Principle, Machine Intelligence 3, Edinburgh University Press, 1968, 77-93. (1968) Zbl0195.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. (1968) MR0252195
  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. (1967) MR0209115
  16. R. Kowalski, An Exposition of Paramodulation with Refinements, Department of Computational Logic, University of Edinburgh, 1968. (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. (1969) MR0275720
  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. (1972) Zbl0246.68017MR0297524
  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. (1972) MR0344089
  20. B. A. Trachtenbrot, Složnosť algoritmov i vyčislenij, Novosibirsk 1967. (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. (1970) 
  22. S. Ju. Masłov, Relationship Between Tactics of the Inverse Method and the Resolution Method, Ibid, 16 (1971), 69-73. (1971) 
  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. (1971) Zbl0263.68049
  24. Orłowska E., Theorem-proving systems, Dissertationes Mathematicae. PWN, Warszawa 1973. (1973) 
  25. M. Loève, Probability Theory, Second Edition. D. van Nostrand Comp., Princeton, New Jersey-Toronto-New York-London 1961. (1961) MR0123342
  26. B. V. Gnedenko, Kurs teoriji verojatnostej, Third Edition, Firmatgiz, Moskva 1961. (1961) 
  27. A. Walde, Sequential Analysis, Russian Translation: Fizmatgiz, Moskva 1960. (1960) MR0116440
  28. E. L. Lehman, Statistical Hypotheses Testing, Russian Translation. Nauka, Moskva 1964. (1964) 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.