|
This article is cited in 4 scientific papers (total in 4 papers)
Mathematical logic, algebra and number theory
The expressiveness of looping terms in the semantic programming
S. Goncharovab, S. Ospichevab, D. Ponomaryovacb, D. Sviridenkoab a Sobolev Institute of Mathematics, 4, Koptyuga ave., Novosibirsk, 630090, Russia
b Novosibirsk State University, 2, Pirogova str., Novosibirsk, 630090, Russia
c Ershov Institute of Informatics Systems, 6, Lavrentyeva ave., Novosibirsk, 630090, Russia
Abstract:
We consider the language of $\Delta_0$-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of $\Delta_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 $\Delta_0$-formulas with bounded recursive terms true in a given list superstructure $HW(\mathcal{M})$ is non-elementary (it contains the class $\mathrm{kExpTime}$, for all $k\geqslant 1$). For $\Delta_0$-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity.
Keywords:
semantic programming, list structures, bounded quantification, reasoning complexity.
Received November 19, 2019, published March 10, 2020
Citation:
S. Goncharov, S. Ospichev, D. Ponomaryov, D. Sviridenko, “The expressiveness of looping terms in the semantic programming”, Sib. Èlektron. Mat. Izv., 17 (2020), 380–394
Linking options:
https://www.mathnet.ru/eng/semr1218 https://www.mathnet.ru/eng/semr/v17/p380
|
Statistics & downloads: |
Abstract page: | 344 | Full-text PDF : | 149 | References: | 17 |
|