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.

Original languageEnglish
Article number024
Pages (from-to)380-394
Number of pages15
JournalСибирские электронные математические известия
Volume17
DOIs
Publication statusPublished - 2020

Keywords

  • Bounded quantification
  • List structures
  • Reasoning complexity
  • Semantic programming
  • semantic programming
  • list structures
  • reasoning complexity
  • bounded quantification

OECD FOS+WOS

  • 1.01 MATHEMATICS

Fingerprint

Dive into the research topics of 'The expressiveness of looping terms in the semantic programming'. Together they form a unique fingerprint.

Cite this