The recognition complexity of decidable theories

I. V. Latkin

Faculty of Basic Engineering Training, D. Serikbayev East Kazakhstan Technical University, 69 Protozanov St., 070004 Ust-Kamenogorsk, Kazakhstan

Abstract: We will find a lower bound on the recognition complexity of the decidable theories that are nontrivial relative to equality, namely, each of these theories is consistent with the formula, whose sense is that there exist at least two distinct elements. However, at first, we will obtain a lower bound on the computational complexity for the first-order theory of the Boolean algebra that contains only two elements. For this purpose, we will code the long-continued deterministic Turing machine computations by the relatively short-length quantified Boolean formulae; the modified Stockmeyer and Meyer method will appreciably be used for this simulation. Then, we will construct a polynomial reduction of this theory to the first-order theory of pure equality.

Keywords and phrases: decidable theories, the theory of equality, the coding of computations, polynomial time, polynomial space, lower complexity bound.

MSC: 03C40, 03C07, 03D15, 68Q05, 68Q15

Received: 11.10.2019

Language: English

DOI: 10.32523/2077-9879-2022-13-1-44-68

Bibliographic databases:

• 
•