English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Semi-unification is the combination of first-order unification andfirst-order matching. The undecidability of semi-unification has been proven byKfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turingmachine immortality (existence of a diverging configuration). The particularTuring reduction is intricate, uses non-computational principles, and involvesvarious intermediate models of computation. The present work gives aconstructive many-one reduction from the Turing machine halting problem tosemi-unification. This establishes RE-completeness of semi-unification undermany-one reductions. Computability of the reduction function, constructivity ofthe argument, and correctness of the argument is witnessed by an axiom-freemechanization in the Coq proof assistant. Arguably, this serves ascomprehensive, precise, and surveyable evidence for the result at hand. Themechanization is incorporated into the existing, well-maintained Coq library ofundecidability proofs. Notably, a variant of Hooper's argument for theundecidability of Turing machine immortality is part of the mechanization.

Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)