TYPE-QUANTIFIER CALCULUS OF POSITIVELY-FORMED FORMULAS WITH NEGATIONS

Cover Page

Cite item

Full Text

Open Access Open Access
Restricted Access Access granted
Restricted Access Subscription Access

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.

About the authors

S. N Vassilyev

Trapeznikov Institute of Control Sciences of RAS

Email: vassilyev_sn@mail.ru
Academician of the RAS Moscow, Russia

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 с.

Supplementary files

Supplementary Files
Action
1. JATS XML
Download

Note

In the print version, the article was published under the DOI: 10.31857/S2686954325030031


Copyright (c) 2025 Russian Academy of Sciences

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

 

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