@article{Schmidt-Schaubeta:2005:DBH:1740735.1740789,
    Address = {Duluth, MN, USA},
    Author = {Schmidt-Schau{\ss}, Manfred and Schulz, Klaus U.},
    ISSN = {0747-7171},
    Journal = {J. Symb. Comput.},
    Keywords = {Bounded unification problems, Decision algorithms, Exponent of periodicity, Higher-order unification, Simply typed lambda calculus},
    Month = {August},
    Number = {2},
    Pages = {905--954},
    Publisher = {Academic Press, Inc.},
    Title = {Decidability of Bounded Higher-order Unification},
    URL = {http://dx.doi.org/10.1016/j.jsc.2005.01.005},
    Volume = {40},
    Year = {2005},
    acmid = {1740789},
    bdsk-url-1 = {http://dx.doi.org/10.1016/j.jsc.2005.01.005},
    date-added = {2013-11-17 13:28:43 +0000},
    date-modified = {2013-11-17 13:28:43 +0000},
    issue_date = {August, 2005},
    numpages = {50},
    doi = {10.1016/j.jsc.2005.01.005}
}

@article{Schmidt-Schaubeta:2005:DBH:1740735.1740789, Address = {Duluth, MN, USA}, Author = {Schmidt-Schau{\ss}, Manfred and Schulz, Klaus U.}, ISSN = {0747-7171}, Journal = {J. Symb. Comput.}, Keywords = {Bounded unification problems, Decision algorithms, Exponent of periodicity, Higher-order unification, Simply typed lambda calculus}, Month = {August}, Number = {2}, Pages = {905--954}, Publisher = {Academic Press, Inc.}, Title = {Decidability of Bounded Higher-order Unification}, URL = {http://dx.doi.org/10.1016/j.jsc.2005.01.005}, Volume = {40}, Year = {2005}, acmid = {1740789}, bdsk-url-1 = {http://dx.doi.org/10.1016/j.jsc.2005.01.005}, date-added = {2013-11-17 13:28:43 +0000}, date-modified = {2013-11-17 13:28:43 +0000}, issue_date = {August, 2005}, numpages = {50}, doi = {10.1016/j.jsc.2005.01.005} }