The expressiveness of looping terms in the semantic programming

The expressiveness of looping terms in the semantic programming Full article

Journal

Сибирские электронные математические известия (Siberian Electronic Mathematical Reports)
, E-ISSN: 1813-3304

Output data

Year: 2020, Volume: 17, Article number : 024, Pages count : 15 DOI: 10.33048/SEMI.2020.17.024

Tags

Bounded quantification; List structures; Reasoning complexity; Semantic programming

Authors

Goncharov S. ^1,2 , Ospichev S. ^1,2 , Ponomaryov D. ^1,2,3 , Sviridenko D. ^1,2

Affiliations

1	Sobolev Institute of Mathematics, 4, Koptyuga ave., Novosibirsk, 630090, Russian Federation
2	Novosibirsk State University, 2, Pirogova str., Novosibirsk, 630090, Russian Federation
3	Ershov Institute of Informatics Systems, 6, Lavrentyeva ave., Novosibirsk, 630090, Russian Federation

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

Web of science:	WOS:000518787600001
Scopus:	2-s2.0-85086915668
OpenAlex:	W3020534824

DB	Citing
Scopus	6
OpenAlex	5
Web of science	2