Standard

The expressiveness of looping terms in the semantic programming. / Goncharov, S.; Ospichev, S.; Ponomaryov, D. et al.

In: Сибирские электронные математические известия, Vol. 17, 024, 2020, p. 380-394.

Research output: Contribution to journal › Article › peer-review

Harvard

Goncharov, S, Ospichev, S, Ponomaryov, D & Sviridenko, D 2020, 'The expressiveness of looping terms in the semantic programming', Сибирские электронные математические известия, vol. 17, 024, pp. 380-394. https://doi.org/10.33048/SEMI.2020.17.024

APA

Goncharov, S., Ospichev, S., Ponomaryov, D., & Sviridenko, D. (2020). The expressiveness of looping terms in the semantic programming. Сибирские электронные математические известия, 17, 380-394. [024]. https://doi.org/10.33048/SEMI.2020.17.024

Vancouver

Goncharov S, Ospichev S, Ponomaryov D, Sviridenko D. The expressiveness of looping terms in the semantic programming. Сибирские электронные математические известия. 2020;17:380-394. 024. doi: 10.33048/SEMI.2020.17.024

Author

Goncharov, S. ; Ospichev, S. ; Ponomaryov, D. et al. / The expressiveness of looping terms in the semantic programming. In: Сибирские электронные математические известия. 2020 ; Vol. 17. pp. 380-394.

BibTeX

@article{ed592e2b842a46089f75ca7425e6e415,
title = "The expressiveness of looping terms in the semantic programming",
abstract = "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.",
keywords = "Bounded quantification, List structures, Reasoning complexity, Semantic programming, semantic programming, list structures, reasoning complexity, bounded quantification",
author = "S. Goncharov and S. Ospichev and D. Ponomaryov and D. Sviridenko",
note = "Funding Information: Goncharov, S., Ospichev, S., Ponomaryov, D., Sviridenko, D., The expressiveness of looping terms in the Semantic Programming. ⃝c 2020 Goncharov S., Ospichev S., Ponomaryov D., Sviridenko D. The authors were supported by the Russian Science Foundation (Grant No. 17-11-01176)",
year = "2020",
doi = "10.33048/SEMI.2020.17.024",
language = "English",
volume = "17",
pages = "380--394",
journal = "Сибирские электронные математические известия",
issn = "1813-3304",
publisher = "Sobolev Institute of Mathematics",

}

RIS

TY - JOUR

T1 - The expressiveness of looping terms in the semantic programming

AU - Goncharov, S.

AU - Ospichev, S.

AU - Ponomaryov, D.

AU - Sviridenko, D.

N1 - Funding Information: Goncharov, S., Ospichev, S., Ponomaryov, D., Sviridenko, D., The expressiveness of looping terms in the Semantic Programming. ⃝c 2020 Goncharov S., Ospichev S., Ponomaryov D., Sviridenko D. The authors were supported by the Russian Science Foundation (Grant No. 17-11-01176)

PY - 2020

Y1 - 2020

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

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

KW - Bounded quantification

KW - List structures

KW - Reasoning complexity

KW - Semantic programming

KW - semantic programming

KW - list structures

KW - reasoning complexity

KW - bounded quantification

UR - http://www.scopus.com/inward/record.url?scp=85086915668&partnerID=8YFLogxK

U2 - 10.33048/SEMI.2020.17.024

DO - 10.33048/SEMI.2020.17.024

M3 - Article

AN - SCOPUS:85086915668

VL - 17

SP - 380

EP - 394

JO - Сибирские электронные математические известия

JF - Сибирские электронные математические известия

SN - 1813-3304

M1 - 024

ER -

ID: 26145642