Pith. sign in

REVIEW

Undecidability in First-Order Theories of Term Algebras Extended with a Substitution Operator

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2111.00573 v1 pith:SZNWIQMA submitted 2021-10-31 math.LO

Juvenal Murwanashyaka This is my paper · ORCID
classification math.LO
keywords undecidablefirst-orderproblemquantifiertheoryalgebrasanaloguebinary
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We introduce a first-order theory of finite full binary trees and then identify decidable and undecidable fragments of this theory. We show that the analogue of Hilbert`s 10th Problem is undecidable by constructing a many-to-one reduction of Post`s Correspondence Problem. By a different method, we show that deciding truth of sentences with one existential quantifier and one bounded universal quantifier is undecidable.

Discussion (0). Continue with ORCID to comment.

Pith tools