В.М. Глушков і автоматизація пошуку доведень теорем в Україні: алгоритм очевидності та системи SAD
DOI:
https://doi.org/10.34121/1028-9763-2020-4-3-10Ключові слова:
V.M. Glushkov, Evidence Algorithm, automated theorem proving, formal natural language, sequent formalism, resolution method, deduction, В.М. Глушков, Алгоритм очевидності, автоматизація пошуку доведень теорем, формальна природна мова, секвенційний формалізм, резолюційний метод, дедукціяАнотація
П'ятдесят років тому, в 1970 році, академік В.М. Глушков опублікував статтю, в якій разом із обговоренням деяких проблем штучного інтелекту сформулював науково-дослідницьку програму під назвою Алгоритм очевидності, що описує його бачення проблеми комп'ютерної підтримки людської діяльності в пошуку ним доведення теорем. В.М. Глушков запропонував зосередити увагу на побудові системи автоматизації пошуку доведень теорем, виконуючи для цього одночасні дослідження у створенні формальних природних мов для запису математичних текстів у звичній для людини формі, побудуванні процедури пошуку доведень на основі машинного поняття очевидності комп’ютерного шагу доведення, яке еволюційно розвивається, використанні знань, заздалегідь відомих або отриманих системою за час її роботи та надання користувачеві інтерфейсних можливостей надати допомогу системі у процесі пошуку нею доведення. З моменту опублікування АО було здійснено дві серйозні спроби реалізації цієї програми. Перша призвела до появи в 1978 році російськомовної системи автоматизації пошуку доведень САД, а друга – до появи в 2002 році її англомовної модифікації під назвою System for Automated Deduction (SAD). Якщо розробку та пробну експлуатацію системи САД було припинено в 1992 році після вилучення з експлуатації ЄС ЕОМ, на яких їх було реалізовано, система SAD, розміщена на веб-сайті nevidal.org, зараз все ще доступна в онлайновому режимі. Тобто у поточний час можна проводити з нею різноманітні експерименти та вирішувати за її допомогою різні задачі, які вимагають точних математичних міркувань. Ця робота присвячена стислому хронологічному опису досліджень із реалізації програми АО за весь період її існування та висвітленню як особливостей систем САД та SAD, так і їх загальних рис та відмінностей. Наведено деякі можливі шляхи подальшого розвитку системи SAD.Посилання
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
18Опубліковано
Номер
Розділ
Ліцензія
Авторське право (c) 2020 Математичні машини і системи
Ця робота ліцензується відповідно до ліцензії Creative Commons Attribution 4.0 International License.
