{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:34Z","timestamp":1747173454818,"version":"3.40.5"},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T00:00:00Z","timestamp":1688515200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2023,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Robinson\u2019s unification algorithm can be identified as the underlying machinery of both C. Meredith\u2019s rule <jats:bold>D<\/jats:bold> (<jats:italic>condensed detachment<\/jats:italic>) in propositional logic and of the construction of <jats:italic>principal types<\/jats:italic> in lambda calculus and combinatory logic. In combinatory logic, it also plays a crucial role in the construction of Meyer, Bunder &amp; Powers\u2019 <jats:italic>Fool\u2019s model<\/jats:italic>. This paper now considers pattern matching, the unidirectional variant of unification, as a basis for logical inference, typing, and a very simple and natural model for untyped combinatory logic. An analysis of the new typing scheme will enable us to characterize a large class of terms of combinatory logic which do not change their principal type when being weakly reduced. We also consider the question whether the major or the minor premisse should be used as the fixed pattern.<\/jats:p>","DOI":"10.1017\/s0960129523000191","type":"journal-article","created":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T11:29:31Z","timestamp":1688556571000},"page":"647-659","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["A (machine-oriented) logic based on pattern matching"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6014-9833","authenticated-orcid":false,"given":"Tim","family":"Lethen","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,7,5]]},"reference":[{"key":"S0960129523000191_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF01371632"},{"key":"S0960129523000191_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/62029.62030"},{"key":"S0960129523000191_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835"},{"key":"S0960129523000191_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BF01048619"},{"key":"S0960129523000191_ref10","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093888116"},{"key":"S0960129523000191_ref12","first-page":"231","article-title":"Correcting a widespread error in unification algorithms","volume":"21","author":"Norvig","year":"1991","journal-title":"Software: Practice and Experience"},{"key":"S0960129523000191_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF01880331"},{"key":"S0960129523000191_ref4","unstructured":"Herbrand, J. (1930). Recherches sur la th\u00e9orie de la d\u00e9monstration. Phd dissertation, University of Paris. Reprinted in: J. Herbrand, \u00c9crits logiques, Paris: Presses Universitaires de France 1968, 35\u2013153. English translation of Chapter 5 in: van Heijenoort, J. (ed.) From Frege to G\u00f6del: a Source Book in Mathematical Logic, 1879\u20131931. Harvard University Press, Cambridge, 1967, 529\u2013567."},{"volume-title":"Prentice Hall Series in Artificial Intelligence","year":"2010","author":"Russell","key":"S0960129523000191_ref16"},{"key":"S0960129523000191_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"volume-title":"Logic: Form and Function \u2013 The Mechanization of Deductive Reasoning","year":"1979","author":"Robinson","key":"S0960129523000191_ref15"},{"volume-title":"Structure and Interpretation of Computer Programs","year":"1984","author":"Abelson","key":"S0960129523000191_ref1"},{"key":"S0960129523000191_ref9","first-page":"215","volume-title":"Philosophical Logic","volume":"1969","author":"Lemmon","year":"1957"},{"key":"S0960129523000191_ref5","unstructured":"Hindley, J. R. (1997). Basic Simple Type Theory, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge."},{"key":"S0960129523000191_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448013"},{"key":"S0960129523000191_ref2","doi-asserted-by":"publisher","DOI":"10.1201\/b11046"},{"key":"S0960129523000191_ref13","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093888213"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000191","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,25]],"date-time":"2023-09-25T10:11:34Z","timestamp":1695636694000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000191\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,5]]},"references-count":17,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["S0960129523000191"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000191","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2023,7,5]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}