Abstract: There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)–(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size
Url:

• https://api.istex.fr/ark:/67375/6H6-9RV9V2SX-N/fulltext.pdf

DOI: 10.1006/inco.2000.2877

---

Links toward previous steps (curation, corpus...)

• to stream Istex, to step Corpus: 001229
• to stream Istex, to step Curation: 001212
• to stream Istex, to step Checkpoint: 002108

---

Links to Exploration step

ISTEX:4DC3AABB35122EF50FB9DF020AE7BC282FDC17DE

---

Le document en format XML

<record>

<TEI wicri:istexFullTextTei="biblStruct">

<teiHeader>

<fileDesc>

<titleStmt>

<title xml:lang="en">On the Undecidability of Second-Order Unification</title>

<author>

<name sortKey="Levy, Jordi" sort="Levy, Jordi" uniqKey="Levy J" first="Jordi" last="Levy">Jordi Levy</name>

</author>

<author>

<name sortKey="Veanes, Margus" sort="Veanes, Margus" uniqKey="Veanes M" first="Margus" last="Veanes">Margus Veanes</name>

</author>

</titleStmt>

<publicationStmt>

<idno type="wicri:source">ISTEX</idno>

<idno type="RBID">ISTEX:4DC3AABB35122EF50FB9DF020AE7BC282FDC17DE</idno>

<date when="2000" year="2000">2000</date>

<idno type="doi">10.1006/inco.2000.2877</idno>

<idno type="url">https://api.istex.fr/ark:/67375/6H6-9RV9V2SX-N/fulltext.pdf</idno>

<idno type="wicri:Area/Istex/Corpus">001229</idno>

<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001229</idno>

<idno type="wicri:Area/Istex/Curation">001212</idno>

<idno type="wicri:Area/Istex/Checkpoint">002108</idno>

<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002108</idno>

<idno type="wicri:doubleKey">0890-5401:2000:Levy J:on:the:undecidability</idno>

<idno type="wicri:Area/Main/Merge">00A436</idno>

</publicationStmt>

<sourceDesc>

<biblStruct>

<analytic>

<title level="a" type="main" xml:lang="en">On the Undecidability of Second-Order Unification</title>

<author>

<name sortKey="Levy, Jordi" sort="Levy, Jordi" uniqKey="Levy J" first="Jordi" last="Levy">Jordi Levy</name>

<affiliation wicri:level="3">

<country wicri:rule="url">Espagne</country>

<wicri:regionArea>Institut d'Investigació en Intel·ligència Artificial, Consejo Superior de Investigaciones Cientı́ficas, Campus UAB, 08193, Bellaterra, Barcelona</wicri:regionArea>

<placeName>

<settlement type="city">Barcelone</settlement>

<region nuts="2" type="region">Catalogne</region>

</placeName>

</affiliation>

</author>

<author>

<name sortKey="Veanes, Margus" sort="Veanes, Margus" uniqKey="Veanes M" first="Margus" last="Veanes">Margus Veanes</name>

<affiliation wicri:level="1">

<country wicri:rule="url">Colombie</country>

<wicri:regionArea>Microsoft Research, One Microsoft Way, Redmond, Washington, 98052</wicri:regionArea>

<wicri:noRegion>98052</wicri:noRegion>

</affiliation>

</author>

</analytic>

<monogr></monogr>

<series>

<title level="j">Information and Computation</title>

<title level="j" type="abbrev">YINCO</title>

<idno type="ISSN">0890-5401</idno>

<imprint>

<publisher>ELSEVIER</publisher>

<date type="published" when="2000">2000</date>

<biblScope unit="volume">159</biblScope>

<biblScope unit="issue">1–2</biblScope>

<biblScope unit="page" from="125">125</biblScope>

<biblScope unit="page" to="150">150</biblScope>

</imprint>

<idno type="ISSN">0890-5401</idno>

</series>

</biblStruct>

</sourceDesc>

<seriesStmt>

<idno type="ISSN">0890-5401</idno>

</seriesStmt>

</fileDesc>

<profileDesc>

<textClass>

<keywords scheme="Teeft" xml:lang="en">

<term>Arity</term>

<term>Base type</term>

<term>Binary function symbol</term>

<term>Comon</term>

<term>Comput</term>

<term>Computer science</term>

<term>Constraint</term>

<term>Context unification</term>

<term>Decidability</term>

<term>Decidable</term>

<term>Degtyarev</term>

<term>Equation systems</term>

<term>Final state</term>

<term>Function symbol</term>

<term>Function symbols</term>

<term>Ganzinger</term>

<term>Goldfarb</term>

<term>Ground rules</term>

<term>Ground sides</term>

<term>Ground term</term>

<term>Ground terms</term>

<term>Gurevich</term>

<term>Initial state</term>

<term>Input alphabet</term>

<term>Input string</term>

<term>Interpolation</term>

<term>Interpolation equations</term>

<term>Lecture notes</term>

<term>Lemma</term>

<term>Linear unification</term>

<term>Maximal arity</term>

<term>Monadic</term>

<term>Monadic sreu</term>

<term>Monadic unification</term>

<term>Normal form</term>

<term>Other cases</term>

<term>Plaisted</term>

<term>Polynomial time equivalent</term>

<term>Polynomial time reduction</term>

<term>Reachability</term>

<term>Reachability constraint</term>

<term>Reachability constraints</term>

<term>Rigid equations</term>

<term>Rigid reachability</term>

<term>Same restriction</term>

<term>Secondorder unification</term>

<term>Simple equations</term>

<term>Solvable</term>

<term>Special cases</term>

<term>Sreu</term>

<term>Substitution</term>

<term>Unary</term>

<term>Undecidability</term>

<term>Undecidable</term>

<term>Unification</term>

<term>Unification problem</term>

<term>Unification problems</term>

<term>Valid computation</term>

<term>Veanes</term>

<term>Voronkov</term>

<term>Word equations</term>

<term>Word unification</term>

</keywords>

</textClass>

<langUsage>

<language ident="en">en</language>

</langUsage>

</profileDesc>

</teiHeader>

<front>

<div type="abstract" xml:lang="en">Abstract: There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)–(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size </div>

</front>

</TEI>

</record>

---

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A436 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00A436 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     ISTEX:4DC3AABB35122EF50FB9DF020AE7BC282FDC17DE
   |texte=   On the Undecidability of Second-Order Unification
}}

---

This area was generated with Dilib version V0.6.33. Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022