Complexity of the decidability of the unquantified set theory with a rank operator |
| |
| Authors: | M. Tetruashvili |
| |
| Affiliation: | (1) Present address: I. Vekua Institute of Applied Mathematics of Tbilisi State University, 2, University St., 380043 Tbilisi, Republic of Georgia |
| |
| Abstract: | The unquantified set theory MLSR containing the symbols ∪, ∖, ≠, ∈,R (R(x) is interpreted as a rank ofx) is considered. It is proved that there exists an algorithm which for any formulaQ of the MLSR theory decides whetherQ is true or not using the spacec|Q|3 (|Q| is the length ofQ). |
| |
| Keywords: | 03D15 |
| 本文献已被 SpringerLink 等数据库收录！ |
|
