- Код статьи
- S2686954325030031-1
- DOI
- 10.31857/S2686954325030031
- Тип публикации
- Статья
- Статус публикации
- Опубликовано
- Авторы
- Том/ Выпуск
- Том 523 / Номер выпуска 1
- Страницы
- 15-20
- Аннотация
- Разработаны логические позитивно-образованные средства представления знаний и автоматизации дедуктивного вывода: типово-кванторные язык и исчисление. В них типовые условия кванторов могут содержать отрицания, а исчисление обладает полнотой относительно выводимости в классическом исчислении предикатов.
- Ключевые слова
- представление знаний логический вывод автоматическое доказательство теорем
- Дата публикации
- 10.06.2025
- Год выхода
- 2025
- Всего подписок
- 0
- Всего просмотров
- 13
Библиография
- 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 с.
