ТИПОВО-КВАНТОРНОЕ ИСЧИСЛЕНИЕ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ С ОТРИЦАНИЯМИ

Обложка

Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

Разработаны логические позитивно-образованные средства представления знаний и автоматизации дедуктивного вывода: типово-кванторные язык и исчисление. В них типовые условия кванторов могут содержать отрицания, а исчисление обладает полнотой относительно выводимости в классическом исчислении предикатов.

Об авторах

С. Н Васильев

Институт проблем управления им. В.А. Трапезникова Российской академии наук

Email: vassilyev_sn@mail.ru
Академик РАН Москва, Россия

Список литературы

  1. Бурбаки Н. Теория множеств. М.: Мир. 1965. 465 с.
  2. Мальцев А.И. Модельные соответствия // Изв. АН СССР. Математика. 1959. 23(3). С. 313–336.
  3. Walther C. Many-sorted unification // J. of the ACM. 1988. 35(1). Р. 1–17.
  4. Palacz W., Grabska E., Slusarczyk G. Ontological Approach to Design Reasoning with the Use of Many-Sorted First Order Logic // Proc. of the 15th Int. Conf. on Artificial Intelligence and Soft Computing. Part II. 2016. Р. 364–374. https://doi.org/10.1007/978-3-319-39384-1_31
  5. Нагул Н.В. Генерация условий сохранения свойств управляемых дискретно-событийных систем // Автоматика и телемеханика. 2016. Выпуск 4. С. 153–172.
  6. Васильев С.Н. Метод сравнения в анализе систем. I–IV // Дифф. уравнения. 1981. 17(9). С. 1562–1573; 1981. 17(11). С. 1945–1954; 1982. 18(2). С. 197–205; 1982. 18(6). С. 938–947.
  7. Vassilyev S.N. Machine synthesis of mathematical theorems // J. Logic Program. 1990. 9(2–3). Р. 235–266.
  8. Васильев С.Н. Об импликации свойств связанных систем: метод получения условий импликации и примеры применения // Изв. РАН. Теория и системы управления. 2020. Выпуск 4. С. 3–17. https://doi.org/10.31857/S0002338820040149
  9. Васильев С.Н., Жерлов А.К. Об исчислении типово-кванторных формул // Докл. РАН. 1995. Т. 343(5). С. 583–585.
  10. Васильев С.Н., Жерлов А.К., Федосова Е.А., Федунов Б.Е. Интеллектное управление динамическими системами. М.: ФИЗМАТЛИТ. 2000. 352 с.
  11. Ларионов А.А., Черкашин Е.А. Программные технологии для эффективного поиска логического вывода в исчислении позитивно-образованных формул. Иркутск: Изд-во ИГУ. 2013. 104 с.
  12. Давыдов А.В., Ларионов А.А., Нагул Н.В. О применении исчисления позитивно-образованных формул для исследования управляемых дискретно-событийных систем // Модел. и анализ информа. систем. 2024. Т. 31(1). С. 54–77. https://doi.org/10.18255/1818-1015-2024-1-54-77
  13. Nagashima Y., Kumar R. A proof strategy language and proof script generation for Isabelle/HOL // Proc. 26th Conf. CADE, LNCS. 2017. Vol. 10395. Р. 528–545. https://doi.org/10.1007/978-3-319-63046-5_32
  14. Робинко Д. Машинно-ориентированная логика, основанная на методе резолюции // Ляпунов А.А., Лупанов О.Б. (ред.). Киберн. сб., Нов. сер. Вып. 7. М.: Мир. 1970. С. 180–218.
  15. Otten J. NanoCoP: a Non-clausal Connection Prover // Proc. Int. Joint Conference on Automated Reasoning. 2016. Р. 302–312.
  16. Мендельсон Э. Введение в математическую логику. М.: Наука, 1971. 320 с.

Дополнительные файлы

Доп. файлы
Действие
1. JATS XML
Скачать

Примечание

В печатной версии статья выходила под DOI: 10.31857/S2686954325030031


© Российская академия наук, 2025

Согласие на обработку персональных данных

 

Используя сайт https://journals.rcsi.science, я (далее – «Пользователь» или «Субъект персональных данных») даю согласие на обработку персональных данных на этом сайте (текст Согласия) и на обработку персональных данных с помощью сервиса «Яндекс.Метрика» (текст Согласия).