Standard

Positive Existential Definability with Unit, Addition and Coprimeness. / Старчак, Михаил Романович.

ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery, 2021. p. 353–360 (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Harvard

Старчак, МР 2021, Positive Existential Definability with Unit, Addition and Coprimeness. in ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation. Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC, Association for Computing Machinery, pp. 353–360, ISSAC 2021 International Symposium on Symbolic and Algebraic Computation, Санкт-Петербург, Russian Federation, 18/07/21. https://doi.org/10.1145/3452143.3465515

APA

Старчак, М. Р. (2021). Positive Existential Definability with Unit, Addition and Coprimeness. In ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation (pp. 353–360). (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC). Association for Computing Machinery. https://doi.org/10.1145/3452143.3465515

Vancouver

Старчак МР. Positive Existential Definability with Unit, Addition and Coprimeness. In ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery. 2021. p. 353–360. (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC). https://doi.org/10.1145/3452143.3465515

Author

Старчак, Михаил Романович. / Positive Existential Definability with Unit, Addition and Coprimeness. ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery, 2021. pp. 353–360 (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC).

BibTeX

@inproceedings{ee8953bf914c42e2bf98a662e2fe3808,
title = "Positive Existential Definability with Unit, Addition and Coprimeness",
abstract = "We consider positively existentially definable sets in the structure 〈ℤ; 1, +, ⊥〉 It is well known that the elementary theory of this structure is undecidable while the existential theory is decidable. We show that after the extension of the signature with the unary '-' functional symbol, binary symbols for dis-equality ≠ and GCD(·, ·) = d for every fixed positive integer d, every positive existential formula in this extended language is equivalent in ℤ to some positive quantifier-free formula. Then we get some corollaries from the main result. The binary order ≤ and dis-coprimeness ⊥ relations are not positively existentially definable in the structure 〈ℤ; 1, +, ⊥〉. Every positively existentially definable set in the structure 〈N; S, ⊥〉 is quantifier-free definable in 〈N; S, ≠, 0, ⊥〉. We also get a decidable fragment of the undecidable ∀∃-Theory of the structure 〈ℤ; 1, +, ≤, |〉, where | is a binary predicate symbol for the integer divisibility relation.",
keywords = "Existential definability, Coprimeness, Quantifier elimination, Decidability, Chinese remainder theorem, chinese remainder theorem, coprimeness, decidability, existential definability, quantifier elimination",
author = "Старчак, {Михаил Романович}",
year = "2021",
month = jul,
day = "18",
doi = "10.1145/3452143.3465515",
language = "English",
series = "Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC",
publisher = "Association for Computing Machinery",
pages = "353–360",
booktitle = "ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation",
address = "United States",
note = "null ; Conference date: 18-07-2021 Through 23-07-2021",
url = "https://issac-conference.org/2021/",

}

RIS

TY - GEN

T1 - Positive Existential Definability with Unit, Addition and Coprimeness

AU - Старчак, Михаил Романович

N1 - Conference code: 46

PY - 2021/7/18

Y1 - 2021/7/18

N2 - We consider positively existentially definable sets in the structure 〈ℤ; 1, +, ⊥〉 It is well known that the elementary theory of this structure is undecidable while the existential theory is decidable. We show that after the extension of the signature with the unary '-' functional symbol, binary symbols for dis-equality ≠ and GCD(·, ·) = d for every fixed positive integer d, every positive existential formula in this extended language is equivalent in ℤ to some positive quantifier-free formula. Then we get some corollaries from the main result. The binary order ≤ and dis-coprimeness ⊥ relations are not positively existentially definable in the structure 〈ℤ; 1, +, ⊥〉. Every positively existentially definable set in the structure 〈N; S, ⊥〉 is quantifier-free definable in 〈N; S, ≠, 0, ⊥〉. We also get a decidable fragment of the undecidable ∀∃-Theory of the structure 〈ℤ; 1, +, ≤, |〉, where | is a binary predicate symbol for the integer divisibility relation.

AB - We consider positively existentially definable sets in the structure 〈ℤ; 1, +, ⊥〉 It is well known that the elementary theory of this structure is undecidable while the existential theory is decidable. We show that after the extension of the signature with the unary '-' functional symbol, binary symbols for dis-equality ≠ and GCD(·, ·) = d for every fixed positive integer d, every positive existential formula in this extended language is equivalent in ℤ to some positive quantifier-free formula. Then we get some corollaries from the main result. The binary order ≤ and dis-coprimeness ⊥ relations are not positively existentially definable in the structure 〈ℤ; 1, +, ⊥〉. Every positively existentially definable set in the structure 〈N; S, ⊥〉 is quantifier-free definable in 〈N; S, ≠, 0, ⊥〉. We also get a decidable fragment of the undecidable ∀∃-Theory of the structure 〈ℤ; 1, +, ≤, |〉, where | is a binary predicate symbol for the integer divisibility relation.

KW - Existential definability

KW - Coprimeness

KW - Quantifier elimination

KW - Decidability

KW - Chinese remainder theorem

KW - chinese remainder theorem

KW - coprimeness

KW - decidability

KW - existential definability

KW - quantifier elimination

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

UR - https://www.mendeley.com/catalogue/e0b4267d-fc48-3ec6-9639-5a5a3bb735a6/

U2 - 10.1145/3452143.3465515

DO - 10.1145/3452143.3465515

M3 - Conference contribution

T3 - Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC

SP - 353

EP - 360

BT - ISSAC 2021 - Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation

PB - Association for Computing Machinery

Y2 - 18 July 2021 through 23 July 2021

ER -

ID: 84459010