The expressiveness of looping terms in the semantic programming Научная публикация
Журнал |
Сибирские электронные математические известия (Siberian Electronic Mathematical Reports)
, E-ISSN: 1813-3304 |
||||||
---|---|---|---|---|---|---|---|
Вых. Данные | Год: 2020, Том: 17, Номер статьи : 024, Страниц : 15 DOI: 10.33048/SEMI.2020.17.024 | ||||||
Ключевые слова | Bounded quantification; List structures; Reasoning complexity; Semantic programming | ||||||
Авторы |
|
||||||
Организации |
|
Реферат:
We consider the language of Δ0-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of Δ0-formulas with non-standard list terms, which represent bounded list search, bounded iteration, and bounded recursion. We prove a number of results on the complexity of model checking and satisfiability for these formulas. In particular, we show that the set of Δ0-formulas with bounded recursive terms true in a given list superstructure HW(M) is non-elementary (it contains the class kExpTime, for all k ≥ 1). For Δ0-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity. © 2020 Goncharov S., Ospichev S., Ponomaryov D., Sviridenko D.
Библиографическая ссылка:
Goncharov S.
, Ospichev S.
, Ponomaryov D.
, Sviridenko D.
The expressiveness of looping terms in the semantic programming
Сибирские электронные математические известия (Siberian Electronic Mathematical Reports). 2020. V.17. 024 :1-15. DOI: 10.33048/SEMI.2020.17.024 WOS Scopus OpenAlex
The expressiveness of looping terms in the semantic programming
Сибирские электронные математические известия (Siberian Electronic Mathematical Reports). 2020. V.17. 024 :1-15. DOI: 10.33048/SEMI.2020.17.024 WOS Scopus OpenAlex
Идентификаторы БД:
Web of science: | WOS:000518787600001 |
Scopus: | 2-s2.0-85086915668 |
OpenAlex: | W3020534824 |