References & Citations
Computer Science > Logic in Computer Science
Title: One is all you need: Second-order Unification without First-order Variables
(Submitted on 16 Apr 2024 (v1), last revised 29 Apr 2024 (this version, v3))
Abstract: We consider the fragment of Second-Order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert's 10$^{th}$ problem is reducible to a \emph{necessary condition} for SOGU unifiability if the signature contains a binary function symbol and two constants, thus proving undecidability. This generalizes known undecidability results, as either first-order variable occurrences or multiple second-order variables were required for the reductions. Furthermore, we show that adding the following restriction:(i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has \emph{bounded congruence}, results in a decidable fragment. The latter fragment is related to \emph{bounded second-order unification} in the sense that the number of bound variable occurrences is a function of the problem structure. We conclude with a discussion concerning the removal of the \emph{bounded congruence} restriction.
Submission history
From: David Cerna [view email][v1] Tue, 16 Apr 2024 14:41:35 GMT (17kb)
[v2] Fri, 26 Apr 2024 10:18:30 GMT (25kb)
[v3] Mon, 29 Apr 2024 05:51:44 GMT (25kb)
Link back to: arXiv, form interface, contact.