Интерактивное порождение новых знаний на основе автоматических средств логического вывода

Интерактивное порождение новых знаний на основе автоматических средств логического вывода

Автор: Васильев С.Н.

Журнал: Онтология проектирования @ontology-of-designing

Рубрика: Общие вопросы формализации проектирования: онтологические аспекты

Статья в выпуске: 1 (47) т.13, 2023 года.

Бесплатный доступ

Работа относится к области представления знаний и алгоритмизации их обработки. Для описания предмета рассмотрения совокупностью утверждений и их обработки используются логические средства первопорядкового типа. В отличие от известных достижений в области автоматического доказательства (АД) в формальных аксиоматических теориях, автоматический синтез текстов утверждений затруднён плохой формализуемостью понятия ценности знания, содержащегося в тексте. В работе на основе развития исчисления позитивно-образованных стандартизованных формул (пос-формул) исследуются возможности автоматизации анализа описания предмета рассмотрения и интерактивного порождения содержательных утверждений для совершенствования этого описания. Предлагаемый метод интерактивного порождения знаний объединяет возможности АД с алгоритмизированным человеко-машинным синтезом текстов новых знаний. АД в исчислении пос-формул помогает человеку не только в анализе свойств, но и в выборе требуемых свойств описания предмета рассмотрения. При выявлении посредством АД отсутствия в анализируемых знаниях свойства, желательного для человека, осуществляется формирование гипотезы, логически гарантирующей наличие требуемого свойства. Автоматически синтезируются в предварительном виде варианты гипотез, дорабатываемые затем интерактивно для повышения содержательности порождаемого текста нового знания. Обосновываются правила синтеза. Их применение продолжает вывод в ситуациях неприменимости базового правила вывода в исчислении пос-формул. Расширение исчисления правилами синтеза преобразует его как первопорядковое исчисление дедуктивного типа в средство дедуктивно-абдуктивного вывода, которое отличается от известных работ, использующих абдукцию, отсутствием ряда ограничений. На иллюстративных примерах показаны представление, анализ и порождение знаний. На этих примерах при интерактивной обработке знаний видна важность наглядности обрабатываемого текста, обеспечиваемой крупноблочной структурой пос-формул, построенных из типовых кванторов. В заключение сформулированы итоги работы и возможные направления развития полученных результатов.

Еще

Представление знаний, порождение знаний, логический синтез гипотез, абдуктивный вывод, автоматическое доказательство теорем

Короткий адрес: https://sciup.org/170198104

IDR: 170198104   |   DOI: 10.18287/2223-9537-2023-13-1-10-28

Список литературы Интерактивное порождение новых знаний на основе автоматических средств логического вывода

  • Мендельсон Э. Введение в математическую логику. М.: Наука, 1971. 320 с.
  • Gentzen G. Untersuchungen uber das logische schliessen // Mathematische Zeitschrift. 1935. Vol.39. P.176-210; D01:10.1007/BF01201353.
  • Маслов CM. Обратный метод установления выводимости в классическом исчислении предикатов // ДАН СССР. 1964. Т.159, №1. С.17-20.
  • Шанин Н.А. Алгоритм машинного поиска естественного логического вывода в исчислении высказываний / Н.А. Шанин, Г.В. Давыдов, С.Ю. Маслов, Г.Е. Минц и др. // М.-Л.: Наука, 1965. 39 c.
  • Робинсон Д. Машинно-ориентированная логика, основанная на методе резолюции // Ляпунов А.А., Лупа-нов О.Б. (ред.). Киберн. сб., Нов. сер. Вып.7. М.: Мир, 1970. С.180-218.
  • D'Agostino M. Handbook of Tableau Methods / M. D'Agostino, D.M. Gabbay, R. Hahnle, J. Posegga, eds. // Dordrecht: Kluwer Academic Publishers, 1999. 680 p.
  • Kovacs L., Voronkov A. First-order theorem proving and Vampire // In: Sharygina, N., Veith, H. (eds.). Proc. of the 25th Conf. on Computer Aided Verification, LNCS. Springer, Heidelberg. 2013. Vol.8044. P.1-35. D0I:10.1007/978-3-642-39799-8_1.
  • Otten J. NanoCoP: a Non-clausal Connection Prover // Proc. Int. Joint Conference on Automated Reasoning. 2016. P.302-312.
  • Васильев С.Н., Жерлов А.К. Об исчислении типово-кванторных формул // Докл. РАН. 1995. Т.343(5). С.583-585.
  • Васильев С.Н., Жерлов А.К., Федосов Е.А., Федунов Б.Е. Интеллектное управление динамическими системами. М.: ФИЗМАТЛИТ, 2000. 352 c.
  • Wang H. Toward mechanical mathematics // IBM J. Res. Develop. 1960. Vol. 4(1). P.2-22.
  • Godel K. Die Vollstandigkeit der Axiome des Logischen Funktionenkalkuls // Monatsh. Math. Phys. 1930. 37. P.349-360.
  • Church A. A Note on the Entscheidungsproblem // J. Symbolic Logic. 1936. 1. P.40-41.
  • Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem // Proc. Lond. Math. Soc., Ser. 2. 1936. 42. P.230-265; 1935. 43. P.544-546.
  • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. 360 c.
  • Черкашин Е.А. Программная система «КВАНТ/1» для автоматического доказательства теорем. Иркутск: ИДСТУ СО РАН, 1999. 16 с.
  • Larionov A.A., Davydov A. V., Cherkashin EA. The calculus of positively constructed formulas, its features, strategies and implementation // In: Proc. of the 36th Intern. Convention on Information and Communication Technology, Electronics and Microelectronics (2013, Opatija, Croatia). N.Y.: IEEE, 2013. P.1023-1028.
  • Давыдов А.В., Ларионов А.А., Черкашин Е.А. Метод трансляции первопорядковых логических формул в позитивно-образованные формулы // Программные продукты и системы. 2019. Т.32(4). С.556-564. D0I:10.15827/0236-235X.128.556-564.
  • Бурбаки Н. Теория множеств. М.: Мир, 1965. 465 с.
  • Мальцев А.И. Модельные соответствия // Изв. АН СССР. Математика. 1959. 23(3). С.313-336.
  • Мальцев А.И. Алгебраические системы. М.: Наука, 1970. 329 с.
  • Walther C. Many-sorted unification // J. of the ACM. 1988. 35(1). P.1-17.
  • Palacz W., Grabska E., Slusarczyk G. 0ntological Approach to Design Reasoning with the Use of Many-Sorted First 0rder Logic // In: Proc. of the 15th Int. Conf. on Artificial Intelligence and Soft Computing (Zakopane, Poland, 2016), Part II, 2016. P.364-374. D0I:10.1007/978-3-319-39384-1_31.
  • Нагул Н.В. Метод логико-алгебраических уравнений в динамике систем // Алгебра и анализ. 2012. 24(4). С.156-181. D0I:10.1090/S1061-0022-2013-01258-1.
  • Нагул Н.В. Генерация условий для сохранения свойств управляемых дискретных систем событий // Автоматика и телемеханика. 2016. 77 (4). С.153-172. DOI: 10.1134/S0005117916040111.
  • Матросов В.М., Анапольский Л.Ю., Васильев С.Н. Метод сравнения в математической теории систем. Новосибирск: Наука, 1980. 481 с.
  • Васильев С.Н. Метод сравнения в анализе систем. I-IV // Дифференциальные уравнения. 1981. 17(9). С.1562-1573; 1981.17(11). С.1945-1954; 1982.18(2). С.197-205; 1982. 18(6). С.938-947.
  • Vassilyev S.N. Machine synthesis of mathematical theorems // J. Logic Program. 1990. 9(2-3). P.235-266.
  • Васильев С.Н. Об импликации свойств связанных систем: метод получения условий импликации и примеры применения // Изв. РАН. Теория и системы управления. 2020. 4. С.3-17. DOI:10.31857/S0002338820040149.
  • Kowalski R. History of Logic Programming. In: Computational Logic, D. Gabbay, J. Woods (eds.). Elsevier. 2014. P.523-569.
  • Horn A. On sentences which are true on direct unions of algebras // J. Symbolic Logic. 1951. 16. P.14-21.
  • Calmerauer A., Kanoui H., Pasero R., Roussel P. Un Systeme de Communication Homme-Machineen Francais // Rapport, Groupe d'lntelligence Artificielle, Universite d'Aix-Marseille II, 1973.
  • Kowalski R. Predicate Logic as a Programming Language // In: Proc. of the IFIP-74 Congress. 1974. P.569-574.
  • Poole D. Representing Diagnosis Knowledge // J. Annals of Mathematics and Artificial Intelligence. 1994. 11. P.33-50.
  • Kobrinskii B.A. Images in Logical-and-Linguistic Artificial Intelligence // J. Biomedical Engineering and Medical Imaging. 2019. 6(1). P.1-8. DOI: 10.14738/jbemi.61.61.61.
  • Buzikov M., Galyaev A., Guryev Yu., Titov K., Yakushenko E., Vassilyev S. Intelligent Control of Autonomous and Anthropocentric On-board Systems // Procedia Computer Science. 2019. 150. P.10-18. DOI:10.1016/j.procs.2019.02.004.
  • Kowalski R., Sadri F. Reactive computing as model generation // New Generat. Comput. 2015. 33: 33-67. DOI:10.1007/s00354-015-0103-z.
  • Lindon R.C. Properties preserved under homomorphism // Pacific J. Math. Vol. 9, 1959. - P. 143-154.
Еще
Статья научная
QR-код для установки приложения SciUp Наведите камеру и скачайте бесплатное приложение SciUp