Computer Science > Logic in Computer Science
[Submitted on 16 Apr 2024 (v1), last revised 5 May 2024 (this version, v4)]
Title:One is all you need: Second-order Unification without First-order Variables
View PDF HTML (experimental)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 UTC (17 KB)
[v2] Fri, 26 Apr 2024 10:18:30 UTC (25 KB)
[v3] Mon, 29 Apr 2024 05:51:44 UTC (25 KB)
[v4] Sun, 5 May 2024 06:22:29 UTC (25 KB)
References & Citations
Bibliographic and Citation Tools
Bibliographic Explorer (What is the Explorer?)
Litmaps (What is Litmaps?)
scite Smart Citations (What are Smart Citations?)
Code, Data and Media Associated with this Article
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub (What is DagsHub?)
Gotit.pub (What is GotitPub?)
Papers with Code (What is Papers with Code?)
ScienceCast (What is ScienceCast?)
Demos
Recommenders and Search Tools
Influence Flower (What are Influence Flowers?)
Connected Papers (What is Connected Papers?)
CORE Recommender (What is CORE?)
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.