Discrete and Continuous Models and Applied Computational ScienceDiscrete and Continuous Models and Applied Computational ScienceDiscrete and Continuous Models and Applied Computational Science2658-46702658-7149Peoples' Friendship University of Russia named after Patrice Lumumba (RUDN University)8591ArticlesСтатьиAutomatic Generation of Logical KnowledgeАвтоматическая генерация логического знанияRautiainenAРаутиайненАКафедра информационных технологий; Российский университет дружбы народов; Peoples' Friendship University of RussiaКафедра информационных технологий; Российский университет дружбы народов-Peoples' Friendship University of RussiaРоссийский университет дружбы народов150420084NO4 (2008)№4 (2008)506008092016Copyright ©; 2008, Раутиайнен А.2008Раутиайнен А.http://creativecommons.org/licenses/by/4.0https://journals.rudn.ru/miph/article/view/8591We study problems which arise deriving generating automatically logical knowledge in systems of artificial intellect, first of all in systems of automatic theorem proving. Three necessary conditions for a generator of logical knowledge are proposed and a verification of these ones is presented.
В статье рассмотрены вопросы, которые возникают при попытке генерации автоматическим образом логического знания в системах искусственного интеллекта, в первую очередь, в системах машинного доказательства теорем. Сформулированы три необходимых требования к подобному генератору и рассмотрено, как их можно выполнить.
автоматическое доказательство теоремискусственный интеллект[Solving Checkers / J. Schaeffer, Y. Bjornsson, N. Burch et al // International Joint Conference on Artificial Intelligence (IJCAI). - 2005. - Pp. 292-297.][Bouzy B., Cazenave T. Computer Go: An AI Oriented Survey // Artificial Intelligence. - Vol. 132, No 1. - 2001.][Korf R. Finding Optimal Solutions to Rubik's Cube Using Pattern Databases // Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97). - Providence, RI: July 2005.][Eich H. P., Ohmann C., Lang K. Decision Support in Acute Abdominal Pain Using an Expert System Fordifferent Knowledge Bases // Tenth IEEE Symposium on Computer-Based Medical Systems, 1997. Proceedings. - 11-13 June 1997.][Toward Automating Airspace Management / G. Taylor, B. Stensrud, S. Eitelman et al // Computational Intelligence for Security and Defense Applications (CISDA). - Honolulu, HI: IEEE Press, 2007.][Validation of an Automated System Model Generator / A. J. Gonzalez, H. R. Myler, F. D. McKenzie et al // IEEE Transactions on Knowledge and Data Engineering. - Vol. 6, No 4. - August 1994.][Стефанюк В. Л. Локальная организация систем - модели и приложения. - M.: Мир, 2004.][Barstow D. R. A Knowledge-Based System for Automatic Program Construction // IJCAI. - 1977. - Pp. 382-388.][Pastre D. A Humanlike Approach for Automatic Theorem Proving // AISB/GI (ECAI). - 1978. - Pp. 248-252.][Pastre D. Knowledge-Based Theorem Proving // GI Jahrestagung. - 1980. - P. 429.][Cohen D. N. Knowledge Based Theorem Proving and Learning. - Ann Arbor: UMI, 1981.][Denzinger J., Schulz S. Recording and Analyzing Knowledge-Based Distributed Deduction Processes // Journal of Symbolic Computation. - Vol. 21. - 1996. -Pp. 523-541.][Denzinger J., Kronenburg M., Schulz S. DISCOUNT. A Distributed and Learning Equational Prover // Journal of Automated Reasoning. - Vol. 18, No 2. - August 1994. - Pp. 189-198.][Lee S. J. An Autonomous Multistrategy Theorem Proving System Using Knowledge-Based Techniques // Journal of Intelligent Information Systems. - Vol. 3, No 1. - August 1994.][Gordon M. From LCF to HOL: a Short History. - Cambridge University, 1996.][Wentzel M. M. Isabelle/Isar - a Versatile Environment for Human-Readable Formal Proof Documents. - Munchen: Institut for Informatik der Technischen, Universitet Munchen, 2001.][Pastre D. Muscadet2.3 : A Knowledge-based Theorem Prover based on Natural Deduction // International Joint Conference on Automated Reasoning IJCAR (Conference on Automated Deduction CADE-JC). - 2001. - Pp. 685-689.][Pagnol J.-P. Modelisation and Automation of Reasoning in Geometry. The ARGOS System: a Learning Companion for High-School Pupils // Proceedings of the 6th International Conference, ITS 2002. - Springer Verlag, 2002.][Раутиаинен А. Алгоритм нумерации объединения конечных множеств без пересечении // XLII Всероссийская конференция по проблемам математики, информатики, физики и химии 17-21 апреля 2006 года: Труды конференции. Секция «Программные исследования». - М.: РУДН, 2006. - С. 122-130.][Paulson L. C. The Isabelle Reference Manual. - Cambridge, United Kingdom:Computer Laboratory, University of Cambridge, 2003.]