УДК 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.
