Relevant Seminars

RSS

Seminar Talk Announcement

  • David Cerna (Czech Academy of Sciences, Institute of Computer Science):

    One is all you need: Second-order Unification without First-order Variables

    05.06.2024 16:00Room 318 (live) and ZOOM @ Institute of Computer Science
    Pod Vodárenskou věží 2
    Praha, 182 00
    Applied Mathematical Logic Seminar

    We consider the fragment of Second-Order unification, referred to as 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 10th problem is reducible to a 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 bounded congruence, results in a decidable fragment. The latter fragment is related to 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 bounded congruence restriction. Joint work with Julian Parsert.

Past Talks