- PII
- S3034504925030031-1
- DOI
- 10.7868/S3034504925030031
- Publication type
- Article
- Status
- Published
- Authors
- Volume/ Edition
- Volume 523 / Issue number 1
- Pages
- 15-20
- Abstract
- Type quantifier language and calculus as logical positively-constructed means of knowledge representation and automation of deductive inference have been developed. In them, the type conditions of quantifiers can contain negations, and the calculus has completeness with respect to derivability in the classical predicate calculus.
- Keywords
- представление знаний логический вывод автоматическое доказательство теорем
- Date of publication
- 02.06.2025
- Year of publication
- 2025
- Number of purchasers
- 0
- Views
- 83
References
- 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 с.
