Glushkov’s evidence algorithm.

*(English. Russian original)*Zbl 1371.68003
Cybern. Syst. Anal. 49, No. 4, 489-500 (2013); translation from Kibern. Sist. Anal. 2013, No. 4, 3-16 (2013).

Summary: Glushkov’s general approaches to the problem of artificial intelligence are considered. In particular, the history of research conducted in line with the Evidence Algorithm program initiated by V. M. Glushkov is described in detail. The results obtained within this program are analyzed.

##### MSC:

68-03 | History of computer science |

68T01 | General topics in artificial intelligence |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

##### Keywords:

evidence algorithm; automated theorem proving; inference search; automated proving system; TL language; ForTheL language
PDF
BibTeX
XML
Cite

\textit{A. A. Letichevsky} et al., Cybern. Syst. Anal. 49, No. 4, 489--500 (2013; Zbl 1371.68003); translation from Kibern. Sist. Anal. 2013, No. 4, 3--16 (2013)

Full Text:
DOI

##### References:

[1] | V. M. Glushkov, ”Some problems of computer engineering and related mathematical problems,” Ukr. Mat. Zhurn., No. 4, 369–376 (1957). · Zbl 0078.12702 |

[2] | V. M. Glushkov, N. M. Grishchenko, and A. A. Stognii, ”Algorithm for the recognition of meaningful sentences,” in: Principles of Construction of Self-Learning Systems [in Russian], Gostekhizdat, Kyiv (1962), pp. 19–26. |

[3] | V. M. Glushkov, Synthesis of Digital Automata [in Russian], Fizmatgiz, Moscow (1962). · Zbl 0104.35404 |

[4] | http://ru.wikipedia.org/wiki/%D0%9C%D0%98%D0%A0 . |

[5] | V. M. Glushkov, V. G. Bodnarchuk, T. A. Grinchenko, et al., ”ANALITIK (algebraic language for the description of computing processes with the use of analytic transformations,” Kibernetika, No. 3, 102–134 (1971). · Zbl 0257.68061 |

[6] | V. M. Glushkov, M. B. Ignat’ev, V. A. Myasnikov, and V. A. Torgashev, Recursive Machines and Computer Facilities [in Russian], Prep. AS USSR, 74–57, Kyiv (1974). |

[7] | V. M. Glushkov, ”Basic architectural principles of increasing computer performance,” in: Probl. Vych. Tekhniki, MTsNTI, Moscow (1981), pp. 6–21. |

[8] | P. C. Gilmore, ”A program for the production of proofs for theorems derivable within the first-order predicate calculus from axioms,” in: Proc. Intern. Conf. Inform. Proces., UNESCO House, Paris (1959), pp. 265–273. |

[9] | Hao Wang, ”Towards mechanical mathematics,” IBM J. Res. and Develop., 4, 2–22 (1960). · Zbl 0097.00404 |

[10] | J. A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, in 2 vols., Elsevier and MIT Press, Cambridge (2001). · Zbl 0964.00020 |

[11] | V. Lifschitz, Mechanical Theorem Proving in the USSR: The Leningrad School, Delphic Assoc., Falls Church (1986). |

[12] | G. Mints, ”Proof theory in the USSR (1925-1970),” J. Symbolic Logic, 56, No. 2, 385–422 (1991). · Zbl 0747.03024 |

[13] | V. M. Glushkov, ”Some problems in the theories of automata and artificial intelligence,” Cybernetics, 6, No. 2, 17–27 (1970). · Zbl 0242.68056 |

[14] | A. Lyaletski, M. Morokhovets, and A. Paskevich, ”Kyiv school of automated theorem proving: A historical chronicle,” in: Logic in Central and Eastern Europe: History, Science and Discourse, Univ. Press of America, Lanham (Md) (2012), pp. 431–469. |

[15] | V. M. Glushkov, ”Smart machines and human mental activity,” Radyans’ka Shkola, No. 2, 87–91 (1962). |

[16] | L. A. Kaluzhnin, ”Information language for mathematics,” in: Applier Linguistics and Machine Translation [in Russian], KNU, Kyiv (1962), pp. 21–29. |

[17] | L. A. Kaluzhin and V. S. Korolyuk, Algorithms and Mathematical Machines [in Ukrainian], Rad. Shkola, Kyiv (1964). |

[18] | F. V. Anufriev, V. V. Fedyurko, A. A. Letichevskii, et al., ”An algorithm for proving theorems in group theory,” Cybernetics, 2, No. 1, 20–25 (1966). |

[19] | V. A. Matulis, ”The first all-Union symposium on automated inference search,” Uspekhi Mat. Nauk, 19, Issue 6(120), 239–241 (1964). |

[20] | F. V. Anufriev, ”Proof search algorithm in set theory,” in: Automata Theory [in Russian], Issue 4, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1967), pp. 3–24. |

[21] | F. V. Anufriev, ”Theorem proving algorithm in logic calculus,” in: Automata Theory [in Russian], Issue 5, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1969), pp. 3–26. |

[22] | A. I. Malashonok, ”Consistency and completeness of the Evidence Algorithm,” in: Automated Theorem Proving in Mathematics [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1974), pp. 75–95. |

[23] | S. Kanger, ”A simplified proof method for elementary logic,” in: P. Braffort and D. Hirschbers (eds.), Computer Programming and Formal Systems, North Holland (1963), pp. 87–93. · Zbl 0217.00902 |

[24] | Z. M. Asel’derov, Solving Equations in Free Groups, Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1968). |

[25] | V. M. Glushkov, V. F. Kostyrko, A. A. Letichevsky, et al., ”A language to write formal theories,” in: Theoretical Cybernetics [in Russian], Issue 3, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1970), pp. 4–31. |

[26] | V. M. Glushkov, Yu. V. Kapitonova, A. A. Letichevsky, K. P. Vershinin, and N. P. Malevanyi, ”Construction of a practical formal language for mathematical theories,” Cybernetics, 8, No. 5, 730–739 (1972). |

[27] | V. M. Glushkov, K. P.Vershinin, Yu. V. Kapitonova, et al., ”A formal language to write mathematical texts,” in: Automated Theorem Proving in Mathematics [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1974), pp. 3–36. |

[28] | K. P. Vershinin, Correctness of Mathematical Texts and its Verification by a Computer, Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1982). |

[29] | A. I. Degtyarev, Methods and Tools for Equality Handling in Automated Theorem Proving, Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1982). |

[30] | A. V. Lyaletski, Automated Proof Search Methods in First-Order Predicate Calculus, Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1982). |

[31] | A. P. Zhezherun, Tools of Computer Processing of Mathematical Texts, Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1980). |

[32] | V. V. Atayan, K. P.Vershinin, and A. P. Zhezherun, ”Structural processing of mathematical texts,” in: Pattern Recognition [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1978), pp. 43–54. |

[33] | A. I. Degtyarev and A.V. Lyaletski, ”Inference in an automated proving system,” in: Mathematical Fundamentals of Artificial Intelligence Systems [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1981), pp. 3–11. |

[34] | M. K. Morokhovets, ”Implementation of inference procedures within the framework of the mathematical text processing system,” in: Automated Processing of Mathematical Texts and Robot Design [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1979), pp. 36–41. |

[35] | V. M. Glushkov, ”The SAD automated proving system: A brief informal presentation,” in: Automated Processing of Mathematical Texts [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1980), pp. 3–30. |

[36] | M. K. Morokhovets, ”On editing inferences,” in: Automated Processing of Mathematical Texts [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1980), pp. 53–61. |

[37] | K. P.Vershinin, ”Search of refutations and ”natural” proofs,” in: Automated Processing of Mathematical Texts and Robot Design [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1979), pp. 12–27. |

[38] | A. V. Lyaletski, ”Generating sufficient statements in the SAD system,” in: Proc. 3rd All-Union Conf. ”Application of mathematical logic methods,” Tallinn, (1983), pp. 65–66. |

[39] | A. I. Degtyarev, ”Monotonous paramodulation strategy,” in: Proc. 5th Conf. on Mathematical Logic, Novosibirsk (1979). |

[40] | V. V. Atayan,”Some tools of the design of information environment in automated proving system,” in: Mathematical Fundamentals of Artificial Intelligence Systems [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1981), pp. 11–17. |

[41] | K. P.Vershinin, ”Application of auxiliary statements during inference search,” Semiotika i Informatika, No. 12, 3–7 (1979). |

[42] | V. V. Atayan and K. P.Vershinin, ”Formalization of some inference search techniques,” in: Automated Processing of Mathematical Texts [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1980), pp. 36–52. |

[43] | K. P.Vershinin and M. K. Morokhovets, ”Application of definitions in automated proving,” in: Software Systems of Inference and Deductive Constructions [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1983), pp 32–41. · Zbl 0562.68069 |

[44] | K. P. Vershinin and M. K. Morokhovets, ”Strategies of the search for derivation of statements with restricted quantifiers,” Cybern. Syst. Analysis, 19, No. 3, 298–308 (1983). · Zbl 0562.68069 |

[45] | M. K. Morokhovets, ”A modified unification procedure,” Cybern. Syst. Analysis, 20, No. 1, 147–152 (1984). · Zbl 0595.03008 |

[46] | M. K. Morokhovets, ”Decision-seeking procedures and transitive relations,” Cybern. Syst. Analysis, 21, No. 5, 702–708 (1985). · Zbl 0648.68097 |

[47] | A.I. Degtyarev, ”Equality handling methods for Horn sets,” in: Methods of Algorithmization and Implementation of Intelligent Problem Solution Processes [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1986), pp. 19–26. |

[48] | T. A. Shevelyuk, ”Term transformation systems in automated theorem proving,” in: Methods of Algorithmization and Implementation of Intelligent Problem Solution Processes [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1986), pp. 26–32. |

[49] | A. A. Vasil’chenko, ”A constructive version of the evidence algorithm for automated program design,” in: Deductive Constructions in Artificial Intelligence Systems and Modeling of Independent Robots [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1987), pp. 76–82. |

[50] | M. K. Morokhovets, ”Many-sorted logics and inference search procedures with regard for quantifier restrictions,” Intellectualization Means for Cybernetic Systems [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1989), pp. 19–27. |

[51] | M. K. Morokhovets, ”Inference search and generalized unification,” in: Proc. All-Union Conf. on Artificial Intelligence, Vol. 1, Pereslavl’-Zalessky (1988), pp. 453–457. |

[52] | V. V. Atayan and M. K. Morokhovets, ”Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system,” Cybern. Syst. Analysis, 32, No. 3, 442–465 (1996). · Zbl 0881.68109 |

[53] | M. K. Morokhovets, Special Theorem Proving Strategy in Mathematics and Means of Their Implementation: Author’s Abstract of PhD Theses, V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1986). |

[54] | V. V. Atayan ”A set of programs to use auxiliary information in theorem proving,” in: Analysis and Processing of Mathematical Texts [in Russian], V. M. Glushkov Institute of Cybernetics AS USSR, Kyiv (1984), pp. 52–60. |

[55] | A. N. Chebotarev and M. K. Morokhovets, ”Consistency checking of automata functional specifications,” Lect. Notes Artific. Intel., 698 (1993), pp. 76–85. · Zbl 0793.68102 |

[56] | K. Vershinin and A. Paskevich, ” ForTheL – the language of formal theories,” J. Inform. Theories and Appl., 7, No. 3, 120–126 (2000). |

[57] | A. Degtyarev, A. Lyaletski, and M. Morokhovets, ”Evidence algorithm and sequent logical inference search,” Lect. Notes Comput. Sci., 1705 (1999), pp. 44–61. · Zbl 0938.03018 |

[58] | A. Lyaletski and A. Paskevich, ”Goal-driven inference search in classical propositional logic,” in: Proc. Intern. Workshop STRATEGIES’2001, Siena, Italy (2001), pp. 65–74. |

[59] | A. Lyaletski, K. Verchinine, A. Degtyarev, and A. Paskevich, ”System for automated deduction (SAD): Linguistic and deductive peculiarities,” in: Adv. Soft Comput., Physica-Verlag, Heidelberg (2002), pp. 413–422. · Zbl 1088.68773 |

[60] | A. V. Lyaletski, A. Paskevich, and K. Verchinine, ”SAD as a mathematical assistant – how should we go from here to there?” J. Applied Logic, 4, No. 4, 560–591 (2006). · Zbl 1107.68099 |

[61] | A. Yu. Paskevich, Formalization Tools for Mathematical Knowledge and Reasoning: Theoretical and Practical Aspects, Author’s Abstract of PhD Theses, T. Shevchenko National University, Kyiv (2005). |

[62] | K. Verchinine, A. Lyaletski, and A. Paskevich, ”System for Automated Deduction (SAD): A tool for proof verification,” Lect. Notes Comput. Sci., 4603, 398–403 (2007). · Zbl 1213.68576 |

[63] | K. Verchinine, A. V. Lyaletski, A. Paskevich, and A. V. Anisimov, ”On correctness of mathematical texts from a logical and practical point of view,” AISC/MKM/Calculemus, 583–598 (2008). · Zbl 1166.68353 |

[64] | A. Lyaletski, ”On some problems of efficient inference search in first-order cut-free modal sequent calculi,” in: Proc. 10th Intern. Symp. on Symbolic and Numeric Algorithms for Scientific Comput., Sept. 2008, Timisoara, Romania, IEEE Inc. (2008), pp. 39–46. |

[65] | J. V. Kapitonova, A. A. Letiñhevsky, and S. V. Konozenko, ”Computations in APS,” Theoret. Comput. Sci., 119, 145–171 (1993). · Zbl 0783.68064 |

[66] | A. Letichevsky and D. Gilbert, ”Model for interaction of agents and environments,” in: D. Bert, C. Choppy, and P. Moses (eds.), Resent Trends in Algebraic Development Techniques; Lect. Notes Comput. Sci., 1827 (1999), pp. 311–328. |

[67] | A. A. Letichevsky, J. V. Kapitonova, V. P. Kotlyarov, et al., ”Insertion modeling in distributed system design,” Probl. Program., No. 4, 13–38, 118 (2008). |

[68] | A. Letichevsky, ”Algebra of behavior transformations and its applications,” Structural Theory of Automata, Semigroups, and Universal Algebra, NATO Science Series, II Mathematics, Physics and Chemistry, 207 (2005), pp. 241–272. · Zbl 1087.68065 |

[69] | V. M. Glushkov, Cybernetics. Computer Engineering. Information Science: Selected Works, Vol. 2 [in Russian], Naukova Dumka, Kyiv (1990), pp. 59–70. · Zbl 0784.68008 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.