V.M. Glushkov and automated theorem proving in Ukraine: evidence algorithm evidence algorithm and SAD systems
DOI:
https://doi.org/10.34121/1028-9763-2020-4-3-10Keywords:
V.M. Glushkov, Evidence Algorithm, automated theorem proving, formal natural language, sequent formalism, resolution method, deduction, В.М. Глушков, Алгоритм очевидності, автоматизація пошуку доведень теорем, формальна природна мова, секвенційний формалізм, резолюційний метод, дедукціяAbstract
Fifty years ago, in 1970, Academician V.M. Glushkov published a paper, in which he, along with a discussion of some problems of artificial intelligence, formulated a research program called Evidence Algorithm describing his vision of the problem of a computer support of human activity in looking for a proof of a particular theorem. V.M. Glushkov proposed to focus attention on the construction of an automated theorem-proving system performing simultaneous investigations in: creating formal natural languages for writing mathematical texts in a form accustomed to a human, constructing a procedure for a proof search based on the evolutionary developing of the machine notion of an evidence of a computer-made proof step, using the knowledge gained by the system during its operation, and providing a user with the opportunity to assist to the system in its proof search process. Since the inception of EA, two serious attempts have been made to implement this program. The first led to the emergence in 1978 of a Russian-language automated theorem proving and the second led to the appearance in 2002 of its English-language modification named System for Automated Deduction (SAD). And if the development and trial operation of the first system were discontinued in 1992 after the output from service of the ES-line computers, on which it was realized, the SAD system, being placed on the website nevidal.org, is now still available in online mode. That is, at the current time, it is possible to carry out different experiments with the SAD system and to solve various problems that require rigorous mathematical reasoning. This work is devoted to a chronological description of studies on the implementation of the EA program for the entire period of its existence and to the highlighting of peculiarities of both the systems, as well as of their common features and distinguishes. Some possible ways of the further development of the SAD system are given.References
1. Глушков В.М. Некоторые проблемы теории автоматов и искусственного интеллекта. Кибернетика. 1970. № 2. С. 3–13.
2. Gilmore P.C. A program for the production of proofs for theorems derivable within the first-order predicate calculus from axioms. International Conference on Information Processing: international conference. Paris, France, 1959. P. 265–273.
3. Wang H. Towards mechanical mathematics. IBM Journal of Research and Development. 1960. Vol. 4. P. 2–22.
4. Robinson J.A. Handbook of Automated Reasoning (in 2 Vol.) / J.A. Robinson, А. Voronkov (eds.). Elsevier and MIT Press, 2001. 2122 p.
5. Lifschitz V. Mechanical theorem proving in the USSR: The Leningrad school. Delphic Associates, Inc., 1986. 206 p.
6. Mints G. Proof theory in the USSR (1925–1970). J. Symbolic Logic. 1991. Vol. 56, N 2. P. 385–422.
7. Lyaletski A., Morokhovets M., Paskevich A. Kyiv school of automated theorem proving: a historical chronicle. Logic in Central and Eastern Europe: History, Science, and Discourse. University Press of America, 2012. P. 376–415.
8. Lyaletski A., Verchinine K. Evidence Algorithm and System for Automated Deduction: A Retrospective View. Intelligent Computer Mathematics (LNAI). 2010. Vol. 6167. P. 411–426.
9. Глушков В.М., Вершинин К.П., Капитонова Ю.В. и др. О формальном языке для записи математических текстов. Автоматизация поиска доказательств теорем в математике. Киев: ИК АН УССР, 1974. С. 3–36.
10. Лялецкий А.В. Методы машинного поиска доказательств в исчислении предикатов первого порядка: автореф. … дис. канд. физ.-мат. наук. Киев: ИК АН УССР, 1982. 23 с.
11. Капитонова Ю.В., Вершинин К.П., Дегтярев А.И., Жежерун А.П., Лялецкий А.В. О системе обработки математических текстов. Кибернетика. 1979. № 2. С. 48.
12. Глушков В.М. Система автоматизации доказательств (САД). Автоматизация обработки математических текстов. Киев: ИК АН УССР, 1980. С. 3–30.
13. Vershinin K., Paskevich A. ForTheL – the language of formal theories. International Journal of Information Theories and Applications. 2000. Vol. 7, N 3. P. 120–126.
14. Degtyarev A., Lyaletski A., Morokhovets M. Evidence Algorithm and sequent logical inference search. Lecture Notes in Computer Science. 1999. Vol. 1705. P. 44–61.
15. Lyaletski A., Paskevich A. Goal-driven inference search in classical propositional logi. Proc. of the International Workshop STRATEGIES'2001. Siena, Italy, 2001. P. 65–74.
16. Lyaletski A., Verchinine K., Degtyarev A., Paskevich A. System for Automated Deduction (SAD): Linguistic and deductive peculiarities. Advances in Soft Computing: the 11th International Symposium IIS 2002 (June 2002). Physica-Verlag, 2002. P. 413–422.
17. Verchinine K., Lyaletski A., Paskevich A. System for Automated Deduction (SAD): a tool for proof verification. Lecture Notes in Computer Science: Proc. of the Conference on Automated Deduction (CADE-21) (Bremen, July 2007). 2007. Vol. 4603. P. 398–403.
18. Konev B., Lyaletski A. Tableau proof search with admissible substitutions. Proc. of the International Workshop on First-order Theorem Proving. Koblenz, Germany, 2005. P. 35–50.
19. Lyaletski A. On some problems of efficient inference search in first-order cut-free modal sequent calculi. Proc. of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. Timisoara, Romania. IEEE Inc., 2008. P. 39–46.
20. Lyaletski А. Evidence Algorithm and inference search in first-order logics. Journal of Automated Reasoning. 2015. Vol. 55, N 3. P. 269–284.
21. Lyaletski А. Mathematical text processing in EA-style: a sequent aspect. Journal of Formalized Reasoning. 2016. Vol. 9, N 1. Р. 235–264.
22. Lyaletski A. Sequent forms of Herbrand theorem and their applications. Annals of Mathematics and Artificial Intelligence. 2006. Vol. 46, N 1–2. P. 191–230.
23. Lyaletski A. (Sr.), Lyaletsky A. (Jr.) Admissible substitutions and Herbrand's theorems for classical and intuitionistic logics. Collegium Logicum. Geodel Centenary 2006: Posters / M. Baaz, N. Preining (eds.). Vienna, Austria. 2006. Vol. IX. P. 41–45.
24. Lyaletski A. Herbrand theorems: the classical and intuitionistic cases. Philosophical Logic (Studies in Logic, Grammar and Rhetoric). 2008. Vol. 14, N 27. P. 101–122.
25. Lyaletski A. On Herbrand-like theorems for cut-free modal sequent logics. Proc. of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania. IEEE Inc., 2009. P. 102–109.
39
18Published
Issue
Section
License
Copyright (c) 2020 Mathematical Machines and Systems
This work is licensed under a Creative Commons Attribution 4.0 International License.
