期刊
SIBERIAN ELECTRONIC MATHEMATICAL REPORTS-SIBIRSKIE ELEKTRONNYE MATEMATICHESKIE IZVESTIYA
卷 17, 期 -, 页码 380-394出版社
SOBOLEV INST MATHEMATICS
DOI: 10.33048/semi.2020.17.024
关键词
semantic programming; list structures; bounded quantification; reasoning complexity
类别
资金
- Russian Science Foundation [17-11-01176]
- Russian Science Foundation [17-11-01176] Funding Source: Russian Science Foundation
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 (M) is non-elementary (it contains the class kExpTime, for all k >= 1). For Delta(0)-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据