{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T11:19:27Z","timestamp":1772450367698,"version":"3.50.1"},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":5398,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1999,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.<\/jats:p>","DOI":"10.2307\/2586506","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:03:01Z","timestamp":1146938581000},"page":"859-880","source":"Crossref","is-referenced-by-count":132,"title":["Unification in intuitionistic logic"],"prefix":"10.1017","volume":"64","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200013682_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BF02945107"},{"key":"S0022481200013682_ref018","first-page":"645\u2013656","article-title":"The universal theory of the free pseudo-Boolean algebra in extended signature","volume":"131","author":"Rybakov","year":"1992","journal-title":"Contemporary Mathematics"},{"key":"S0022481200013682_ref013","first-page":"911\u2013939","volume":"60","author":"Ghilardi","year":"1995","journal-title":"A sheaf representation and duality for finitely presented Heyting algebras"},{"key":"S0022481200013682_ref012","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.6.733"},{"key":"S0022481200013682_ref009","unstructured":"Ghilardi S. , E-unification in some varieties of Heyting algebras, in preparation."},{"key":"S0022481200013682_ref006","first-page":"31\u201342","volume":"34","author":"Fine","year":"1974","journal-title":"Logics containing K4, Part I"},{"key":"S0022481200013682_ref002","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1970-0256952-1"},{"key":"S0022481200013682_ref011","volume-title":"Quaderno n. 58\/96","author":"Ghilardi","year":"1996"},{"key":"S0022481200013682_ref005","first-page":"498\u2013504","volume":"60","author":"de Jongh","year":"1995","journal-title":"The decidability of dependency in intuitionistic propositional logic"},{"key":"S0022481200013682_ref017","first-page":"912\u2013923","volume":"57","author":"Rybakov","year":"1992","journal-title":"Rules of inference with parameters for intuitionistic logic"},{"key":"S0022481200013682_ref004","first-page":"187\u2013213","volume-title":"Logic: from foundations to applications","author":"de Jongh","year":"1996"},{"key":"S0022481200013682_ref015","first-page":"33\u201352","volume":"57","author":"Pitts","year":"1992","journal-title":"On an interpretation of second order quantification in first order intuitionistic propositional logic"},{"key":"S0022481200013682_ref016","first-page":"428\u2013431","article-title":"Equations in a free topoboolean algebra and substitution problem","volume":"33","author":"Rybakov","year":"1986","journal-title":"Soviet Math, Dokl"},{"key":"S0022481200013682_ref022","first-page":"225\u2013339","volume-title":"Handbook of philosophical logic","volume":"III","author":"van Dalen","year":"1986"},{"key":"S0022481200013682_ref010","first-page":"240\u2013244","article-title":"Free Heyting algebras as bi-Heyting algebras","volume":"XIV","author":"Ghilardi","year":"1992","journal-title":"Mathematical Reports of the Academy of Sciences of Canada"},{"key":"S0022481200013682_ref023","volume-title":"Logic Group Preprint Series 161","author":"Visser","year":"1996"},{"key":"S0022481200013682_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2977-2"},{"key":"S0022481200013682_ref001","first-page":"41\u2013125","volume-title":"Handbook of logic in artificial intelligence and logic programming","author":"Baader","year":"1993"},{"key":"S0022481200013682_ref007","first-page":"619\u2013651","volume":"50","author":"Fine","year":"1985","journal-title":"Logics containing K4, Part II"},{"key":"S0022481200013682_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0435-0"},{"key":"S0022481200013682_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80012-4"},{"key":"S0022481200013682_ref003","first-page":"51\u201364","volume-title":"The L. E. J. Brouwer centenary symposium","author":"de Jongh","year":"1982"},{"key":"S0022481200013682_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80013-6"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200013682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T21:17:57Z","timestamp":1557436677000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200013682\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,6]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,6]]}},"alternative-id":["S0022481200013682"],"URL":"https:\/\/doi.org\/10.2307\/2586506","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,6]]}}}