UDC 004.8:519.7
EVIDENCE ALGORITHM AND SAD SYSTEMS:
PAST AND POSSIBLE FUTURE
Abstract. The paper is devoted to the Evidence Algorithm programme on automated reasoning initiated
by Academician Glushkov in 1970 and found its expression in the form of the Russian-language and English-language
SAD systems intended for automated deduction. Some of their characteristic peculiarities and features are described.
Examples demonstrating the possibility of their use for solving mathematical and common problems that require
deductive constructions are supplied. Possible ways of the further development of the English-language SAD system are given.
Keywords: Evidence Algorithm, SAD system, automated reasoning, automated theorem proving, prover.
FULL TEXT
REFERENCES
- 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.
