{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:30:57Z","timestamp":1784845857478,"version":"3.55.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,7,3]],"date-time":"2021-07-03T00:00:00Z","timestamp":1625270400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,7,3]],"date-time":"2021-07-03T00:00:00Z","timestamp":1625270400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10472-021-09764-0","type":"journal-article","created":{"date-parts":[[2021,7,3]],"date-time":"2021-07-03T21:02:16Z","timestamp":1625346136000},"page":"523-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The undecidability of proof search when equality is a logical connective"],"prefix":"10.1007","volume":"90","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0274-4954","authenticated-orcid":false,"given":"Dale","family":"Miller","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Viel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,3]]},"reference":[{"issue":"1","key":"9764_CR1","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2071368.2071370","volume":"13","author":"D Baelde","year":"2012","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput Logic 13(1), 2:1\u20132:44 (2012)","journal-title":"ACM Trans. Comput Logic"},{"issue":"2","key":"9764_CR2","first-page":"1","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y., Abella: A system for reasoning about relational specifications. J. Formal. Reason. 7(2), 1\u201389 (2014)","journal-title":"J. Formal. Reason."},{"key":"9764_CR3","doi-asserted-by":"crossref","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pp 391\u2013397. Springer, New York (2007)","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"9764_CR4","doi-asserted-by":"crossref","unstructured":"Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: Intensional negation of logic programs examples and implementation techniques. In: Proc. of the TAPSOFT \u201987, Number 250 in LNCS, pp 96\u2013110. Springer (1987)","DOI":"10.1007\/BFb0014975"},{"key":"9764_CR5","doi-asserted-by":"publisher","first-page":"354","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58, 354\u2013363 (1936)","journal-title":"Am. J. Math."},{"key":"9764_CR6","doi-asserted-by":"crossref","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, J., Minker, J. (eds.) Logic and Data Bases, pp 293\u2013322. Plenum Press, New York (1978)","DOI":"10.1007\/978-1-4684-3384-5_11"},{"issue":"1-3","key":"9764_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF01531022","volume":"6","author":"WM Farmer","year":"1992","unstructured":"Farmer, W.M.: The Kreisel length-of-proof problem. Ann. Math. Artif. Intell 6(1-3), 27\u201355 (1992)","journal-title":"Ann. Math. Artif. Intell"},{"issue":"1","key":"9764_CR8","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.ic.2010.09.004","volume":"209","author":"A Gacek","year":"2011","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48\u201373 (2011)","journal-title":"Inf. Comput."},{"key":"9764_CR9","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"JH Gallier","year":"1986","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)"},{"key":"9764_CR10","unstructured":"Gallier, J.H., Raatz, S., Snyder, W.: Theorem Proving Using Rigid E-unification: Equational Matings. In: 2nd Symp. on Logic in Computer Science, pp 338\u2013346. IEEE Computer Society Press, Washington (1987)"},{"key":"9764_CR11","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969, pp 68\u2013131. North-Holland, Amsterdam (1935)","DOI":"10.1016\/S0049-237X(08)70822-X"},{"issue":"1","key":"9764_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"9764_CR13","unstructured":"Girard, J.-Y.: A fixpoint theorem in linear logic an email posting archived at https:\/\/www.seas.upenn.edu\/sweirich\/types\/archive\/1992\/msg00030.html to the linear@cs.stanford.edumailing list (1992)"},{"key":"9764_CR14","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W Goldfarb","year":"1981","unstructured":"Goldfarb, W.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225\u2013230 (1981)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"9764_CR15","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1007\/s10817-018-9475-3","volume":"63","author":"Q Heath","year":"2019","unstructured":"Heath, Q., Miller, D.: A proof theory for model checking. J. Automat. Reason. 63(4), 857\u2013885 (2019)","journal-title":"J. Automat. Reason."},{"key":"9764_CR16","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"GP Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed \u03bb-calculus. Theor. Comput. Sci. 1, 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9764_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J Kraj\u00edcek","year":"1988","unstructured":"Kraj\u00edcek, J., Pudl\u00e1k, P.: The number of proof lines and the size of proofs in first order logic. Arch. Math. Log 27(1), 69\u201384 (1988)","journal-title":"Arch. Math. Log"},{"key":"9764_CR18","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite rational and infinite trees. In: 3nd Symp. on Logic in Computer Science, pp 348\u2013357 (1988)"},{"key":"9764_CR19","doi-asserted-by":"crossref","unstructured":"Matiyasevich, Y.: Hilbert\u2019s tenth problem and paradigms of computation. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) CiE: Computing in Europe, number 3526 in LNCS, pp 310\u2013321. Springer (2005)","DOI":"10.1007\/11494645_39"},{"key":"9764_CR20","volume-title":"Hilbert\u2019s Tenth Problem","author":"YV Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s Tenth Problem. MIT Press, Cambridge (1993)"},{"key":"9764_CR21","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theor. Comput. Sci. 232, 91\u2013119 (2000)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"9764_CR22","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Computat. 1(4), 497\u2013536 (1991)","journal-title":"J. Logic Computat."},{"issue":"4","key":"9764_CR23","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14 (4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"9764_CR24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order logic. Cambridge University Press, Cambridge (2012)"},{"issue":"4","key":"9764_CR25","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Computat. Logic 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Computat. Logic"},{"issue":"4","key":"9764_CR26","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1145\/937555.937559","volume":"4","author":"A Momigliano","year":"2003","unstructured":"Momigliano, A., Pfenning, F.: Higher-order pattern complement and strict \u03bb-calculus. ACM Trans. Computat. Logic 4(4), 493\u2013529 (2003)","journal-title":"ACM Trans. Computat. Logic"},{"issue":"1","key":"9764_CR27","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00881902","volume":"11","author":"G Nadathur","year":"1993","unstructured":"Nadathur, G.: A proof procedure for the logic of hereditary Harrop formulas. J. Autom. Reason. 11(1), 115\u2013145 (1993)","journal-title":"J. Autom. Reason."},{"key":"9764_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. Number 828 in science & business media springer, Berlin (1994)"},{"key":"9764_CR29","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) 8th Symp. on Logic in Computer Science, pp 222\u2013232. IEEE Computer Society Press, IEEE, Piscataway (1993)"},{"key":"9764_CR30","first-page":"230","volume":"42","author":"AM Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42, 230\u2013265 (1936)","journal-title":"Proc. Lond. Math. Soc."},{"key":"9764_CR31","unstructured":"Viel, A., Miller, D.: Proof search when equality is a logical connective Unpublished draft presented to the International Workshop on Proof-Search in Type Theories (2010)"},{"issue":"1-2","key":"9764_CR32","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/S0304-3975(98)00317-X","volume":"224","author":"A Voronkov","year":"1999","unstructured":"Voronkov, A.: Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Theor. Comput. Sci. 224(1-2), 319\u2013352 (1999)","journal-title":"Theor. Comput. Sci."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09764-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-021-09764-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09764-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T08:32:44Z","timestamp":1651134764000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-021-09764-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,3]]},"references-count":32,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["9764"],"URL":"https:\/\/doi.org\/10.1007\/s10472-021-09764-0","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,3]]},"assertion":[{"value":"21 June 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 July 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}