УДК 004.8:519.7
АЛГОРИТМ ОЧЕВИДНОСТИ І СИСТЕМИ SAD: МИНУЛЕ ТА МОЖЛИВЕ МАЙБУТНЄ
Анотація. Роботу присвячено програмі «Алгоритм Очевидності», що була ініційована академіком В. М. Глушковим
у 1970 році і знайшла своє втілення у вигляді російськомовної та англомовної систем SAD,
призначе-них для автоматизованого проведення дедукції. Надано опис їхніх характер-них рис та особливостей.
Наведено приклади, які демонструють можливість їх використання для розв’язання математичних і повсякденних задач,
що потребують виконання дедуктивних побудов. Описано можливі шляхи по-дальшого розвитку англомовної системи SAD.
Ключові слова: Алгоритм Очевидності, система SAD, автоматизація мірку-вань, автоматизація пошуку доведень теорем, прувер.
ПОВНИЙ ТЕКСТ
Lyaletski Alexander Vadimovich,
Candidate of Physical and Mathematical Sciences, Senior Researcher, National University of Life and Environmental Sciences of Ukraine, Kyiv,
a.lyaletski@nubip.edu.ua
СПИСОК ЛІТЕРАТУРИ
- Glushkov V.M. Some problems in the theories of automata and artificial intelligence. Cybernetics and Systems Analysis. 1970. Vol. 6, N 2. P. 17–27. https://doi.org/10.1007/BF01070496.
- 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. Lanham (Md): University Press of America, 2012. P. 431–469.
- Vershinine K., Paskevich A. ForTheL — the language of formal theories. International Journal of Information Theories and Applications. 2000. Vol. 7, N 3. P. 120–126.
- Glushkov V.M., Kapitonova Yu.V., Letichevskii A.A., Vershinin K.P., Malevanyi N.P. Construction of a practical formal language for mathematical theories. Cybernetics and Systems Analysis. 1972. Vol. 8, N 5, P. 730–739. https://doi.org/10.1007/BF01068445.
- Otter homepage. URL: http://www.mcs.anl.gov/research/projects/other/.
- SPASS theorm prover. URL: https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/ spass-workbench/.
- Vampire's homepage. URL: http://www.vprover.org/.
- The E Theorem Prover. URL: https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html.
- Lyaletski A. Evidence Algorithm and inference search in first-order logics. Journal of Automated Reasoning. 2015. Vol. 55. P. 269–284.
- Kanger S. A simplified proof method for elementary logic. In: Computer Programming and Formal Systems. Braffort P., Hirchberg D. (Eds.). Amsterdam: North-Holland Publishing Company, 1963. P. 87–94.
- Lyaletski A. Mathematical text processing in EA-style: a sequent aspect. Journal of Formalized Reasoning (Special Issue: Twenty Years of the QED Manifesto). 2016. Vol. 9, N 1. P. 235–264.
- Paskevich A., Verchinine K., Lyaletski A., Anisimov A. Reasoning inside a formula and ontological correctness of a formal mathematical text. In: Calculemus/MKM 2007 Work in Progress, RISC-Linz Report Series. Kauers M., Kerber M., Miner R., Windsteiger W. (Eds.). Hagenberg, Austria. 2007. Vol. 07-06. P. 77–91.
