{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T15:32:43Z","timestamp":1775489563257,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030887001","type":"print"},{"value":"9783030887018","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88701-8_8","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"126-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Algorithmic Correspondence for Relevance Logics, Bunched Implication Logics, and Relation Algebras via an Implementation of the Algorithm PEARL"],"prefix":"10.1007","author":[{"given":"Willem","family":"Conradie","sequence":"first","affiliation":[]},{"given":"Valentin","family":"Goranko","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Jipsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"issue":"4","key":"8_CR1","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/s10992-017-9445-y","volume":"47","author":"G Badia","year":"2018","unstructured":"Badia, G.: On Sahlqvist formulas in relevant logic. J. Philos. Log. 47(4), 673\u2013691 (2018)","journal-title":"J. Philos. Log."},{"key":"8_CR2","unstructured":"van Benthem, J.: Modal correspondence theory. Ph.D. thesis, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam (1976)"},{"key":"8_CR3","unstructured":"van Benthem, J.: A note on dynamic arrow logic. Technical report LP-92-11, ILLC, University of Amsterdam (1992)"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 3, 2nd edn., pp. 325\u2013408. Springer, Dordrecht (2001). https:\/\/doi.org\/10.1007\/978-94-017-0454-0_4","DOI":"10.1007\/978-94-017-0454-0_4"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1017\/S1755020309090145","volume":"2","author":"K Bimb\u00f3","year":"2009","unstructured":"Bimb\u00f3, K., Dunn, J.M., Maddux, R.D.: Relevance logics and relation algebras. Rev. Symb. Log. 2(1), 102\u2013131 (2009)","journal-title":"Rev. Symb. Log."},{"key":"8_CR6","series-title":"Outstanding Contributions to Logic","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1007\/978-3-319-06025-5_36","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"W Conradie","year":"2014","unstructured":"Conradie, W., Ghilardi, S., Palmigiano, A.: Unified correspondence. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics. OCL, vol. 5, pp. 933\u2013975. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06025-5_36"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Conradie, W., Goranko, V.: Algorithmic correspondence for relevance logics I. The algorithm PEARL. In: D\u00fcntsch, I., Mares, E. (eds.) Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs, pp. 163\u2013209. Springer, Heidelberg (2021). https:\/\/www2.philosophy.su.se\/goranko\/papers\/PEARL.pdf","DOI":"10.1007\/978-3-030-71430-7_4"},{"key":"8_CR8","unstructured":"Conradie, W., Goranko, V., Jipsen, P.: Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (2021). Technical report https:\/\/arxiv.org\/abs\/2108.06603"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic, I. The core algorithm SQEMA. Log. Methods Comput. Sci. 2(1:5), 1\u201326 (2006)","DOI":"10.2168\/LMCS-2(1:5)2006"},{"issue":"3","key":"8_CR10","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/j.apal.2011.10.004","volume":"163","author":"W Conradie","year":"2012","unstructured":"Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for distributive modal logic. Ann. Pure Appl. Logic 163(3), 338\u2013376 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"9","key":"8_CR11","doi-asserted-by":"publisher","first-page":"923","DOI":"10.1016\/j.apal.2019.04.003","volume":"170","author":"W Conradie","year":"2019","unstructured":"Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for non-distributive logics. Ann. Pure Appl. Logic 170(9), 923\u2013974 (2019). https:\/\/doi.org\/10.1016\/j.apal.2019.04.003","journal-title":"Ann. Pure Appl. Logic"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2017.07.002","volume":"93","author":"F Dahlqvist","year":"2017","unstructured":"Dahlqvist, F., Pym, D.: Coalgebraic completeness-via-canonicity for distributive substructural logics. J. Log. Algebr. Methods Program. 93, 1\u201322 (2017). https:\/\/doi.org\/10.1016\/j.jlamp.2017.07.002","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF01058532","volume":"54","author":"M de Rijke","year":"1995","unstructured":"de Rijke, M., Venema, Y.: Sahlqvist\u2019s theorem for Boolean algebras with operators with an application to cylindric algebras. Stud. Log. 54(1), 61\u201378 (1995). https:\/\/doi.org\/10.1007\/BF01058532","journal-title":"Stud. Log."},{"key":"8_CR14","unstructured":"Doumane, A., Pous, D.: Non axiomatisability of positive relation algebras with constants, via graph homomorphisms. In: Konnov, I., Kov\u00e1cs, L. (eds.) Proceedings of CONCUR 2020. LIPIcs, vol. 171, pp. 29:1\u201329:16. Schloss Dagstuhl (2020)"},{"key":"8_CR15","series-title":"Outstanding Contributions to Logic","doi-asserted-by":"publisher","first-page":"881","DOI":"10.1007\/978-3-319-06025-5_34","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"JM Dunn","year":"2014","unstructured":"Dunn, J.M.: Arrows pointing at arrows: arrow logic, relevance logic, and relation algebras. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics. OCL, vol. 5, pp. 881\u2013894. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06025-5_34"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"713","DOI":"10.2178\/jsl\/1122038911","volume":"70","author":"JM Dunn","year":"2005","unstructured":"Dunn, J.M., Gehrke, M., Palmigiano, A.: Canonical extensions and relational completeness of some substructural logics. J. Symb. Logic 70, 713\u2013740 (2005)","journal-title":"J. Symb. Logic"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-94-017-0460-1_1","volume-title":"Handbook of Philosophical Logic","author":"J Dunn","year":"2002","unstructured":"Dunn, J., Restall, G.: Relevance logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. HALO, vol. 6, 2nd edn., pp. 1\u2013128. Springer, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-017-0460-1_1","edition":"2"},{"key":"8_CR18","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"N Galatos","year":"2007","unstructured":"Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier, Amsterdam (2007)"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.apal.2004.04.007","volume":"131","author":"M Gehrke","year":"2005","unstructured":"Gehrke, M., Nagahashi, H., Venema, Y.: A Sahlqvist theorem for distributive modal logic. Ann. Pure Appl. Logic 131, 65\u2013102 (2005)","journal-title":"Ann. Pure Appl. Logic"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Gehrke, M., J\u00f3nsson, B.: Bounded distributive lattice expansions. Mathematica Scandinavica 94(1), 13\u201345 (2004)","DOI":"10.7146\/math.scand.a-14428"},{"issue":"5","key":"8_CR21","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1093\/logcom\/11.5.737","volume":"11","author":"V Goranko","year":"2001","unstructured":"Goranko, V., Vakarelov, D.: Sahlqvist formulae in hybrid polyadic modal languages. J. Log. Comput. 11(5), 737\u2013754 (2001)","journal-title":"J. Log. Comput."},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1142\/9789812776471_0012","volume-title":"Advances in Modal Logic","author":"V Goranko","year":"2002","unstructured":"Goranko, V., Vakarelov, D.: Sahlqvist formulas unleashed in polyadic modal languages. In: Wolter, F., Wansing, H., de Rijke, M., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 3, pp. 221\u2013240. World Scientific, Singapore (2002)"},{"issue":"1\u20132","key":"8_CR23","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.apal.2005.10.005","volume":"141","author":"V Goranko","year":"2006","unstructured":"Goranko, V., Vakarelov, D.: Elementary canonical formulae: extending Sahlqvist\u2019s theorem. Ann. Pure Appl. Logic 141(1\u20132), 180\u2013217 (2006)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1017\/S1755020310000249","volume":"4","author":"R Hirsch","year":"2011","unstructured":"Hirsch, R., Mikul\u00e1s, S.: Positive fragments of relevance logic and algebras of binary relations. Rev. Symb. Log. 4(1), 81\u2013105 (2011)","journal-title":"Rev. Symb. Log."},{"issue":"4","key":"8_CR25","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/BF01057646","volume":"53","author":"B J\u00f3nsson","year":"1994","unstructured":"J\u00f3nsson, B.: On the canonicity of Sahlqvist identities. Studis Logica 53(4), 473\u2013491 (1994). https:\/\/doi.org\/10.1007\/BF01057646","journal-title":"Studis Logica"},{"key":"8_CR26","unstructured":"Kowalski, T.: Relevant logic and relation algebras. In: Galatos, N., Kurz, A., Tsinakis, C. (eds.) TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic. EPiC Series in Computing, vol. 25, pp. 125\u2013128 (2014)"},{"key":"8_CR27","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1090\/S0002-9947-1982-0662049-7","volume":"272","author":"R Maddux","year":"1982","unstructured":"Maddux, R.: Some varieties containing relation algebras. Trans. Am. Math. Soc. 272, 501\u2013526 (1982)","journal-title":"Trans. Am. Math. Soc."},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Maddux, R.D.: Relevance logic and the calculus of relations. Rev. Symb. Log. 3(1), 41\u201370 (2010). https:\/\/doi.org\/10.1017\/S1755020309990293","DOI":"10.1017\/S1755020309990293"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Top down operator precedence. In: Fischer, P.C., Ullman, J.D. (eds.) Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, October 1973, pp. 41\u201351. ACM Press (1973)","DOI":"10.1145\/512927.512931"},{"key":"8_CR30","series-title":"Applied Logic Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"D Pym","year":"2002","unstructured":"Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. APLS, vol. 26. Springer, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-017-0091-7"},{"key":"8_CR31","unstructured":"Routley, R., Meyer, R., Plumwood, V., Brady, R.: Relevant Logics and its Rivals (Volume I). Ridgeview, CA (1982)"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Sahlqvist, H.: Correspondence and completeness in the first and second-order semantics for modal logic. In: Kanger, S. (ed.) Proceedings of the 3rd Scandinavian Logic Symposium, Uppsala 1973, pp. 110\u2013143. Springer, Amsterdam (1975). https:\/\/doi.org\/10.1016\/S0049-237X(08)70728-6","DOI":"10.1016\/S0049-237X(08)70728-6"},{"issue":"3","key":"8_CR33","doi-asserted-by":"publisher","first-page":"992","DOI":"10.2307\/2274758","volume":"54","author":"G Sambin","year":"1989","unstructured":"Sambin, G., Vaccaro, V.: A new proof of Sahlqvist\u2019s theorem on modal definability and completeness. J. Symb. Log. 54(3), 992\u2013999 (1989)","journal-title":"J. Symb. Log."},{"issue":"3","key":"8_CR34","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1023335229747","volume":"73","author":"T Seki","year":"2003","unstructured":"Seki, T.: A Sahlqvist theorem for relevant modal logics. Stud. Logica. 73(3), 383\u2013411 (2003)","journal-title":"Stud. Logica."},{"issue":"1","key":"8_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S1755020310000201","volume":"4","author":"T Suzuki","year":"2011","unstructured":"Suzuki, T.: Canonicity results of substructural and lattice-based logics. Rev. Symb. Log. 4(1), 1\u201342 (2011). https:\/\/doi.org\/10.1017\/S1755020310000201","journal-title":"Rev. Symb. Log."},{"issue":"2","key":"8_CR36","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1017\/S1755020313000026","volume":"6","author":"T Suzuki","year":"2013","unstructured":"Suzuki, T.: A Sahlqvist theorem for substructural logic. Rev. Symb. Log. 6(2), 229\u2013253 (2013). https:\/\/doi.org\/10.1017\/S1755020313000026","journal-title":"Rev. Symb. Log."},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Urquhart, A.: Duality for algebras of relevant logics. Studia Logica 56(1\/2), 263\u2013276 (1996). https:\/\/doi.org\/10.1007\/BF00370149","DOI":"10.1007\/BF00370149"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88701-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T00:49:26Z","timestamp":1634863766000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marseille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics19.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}