{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:26Z","timestamp":1762459466402,"version":"3.37.3"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Ministry of Education, Culture, Sports, Science, and Technology (JP)","award":["16812096"],"award-info":[{"award-number":["16812096"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We develop an abstract proof calculus for hybrid logics whose sentences are (\n            <jats:italic>hybrid<\/jats:italic>\n            )\n            <jats:italic>Horn clauses<\/jats:italic>\n            , and we prove a\n            <jats:italic>Birkhoff completeness<\/jats:italic>\n            theorem for hybrid logics in the general setting provided by the\n            <jats:italic>institution theory<\/jats:italic>\n            . This result is then applied to particular cases of hybrid logics with user-defined sharing, where the first-order variables in quantified sentences are interpreted uniformly across worlds.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0414-y","type":"journal-article","created":{"date-parts":[[2017,1,31]],"date-time":"2017-01-31T07:19:55Z","timestamp":1485847195000},"page":"805-832","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Birkhoff style calculi for hybrid logics"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0978-2200","authenticated-orcid":false,"given":"Daniel","family":"G\u0103in\u0103","sequence":"first","affiliation":[{"name":"Institute of Mathematics for Industry, Kyushu University, Fukuoka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.5.657"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.02.005"},{"issue":"2","key":"e_1_2_1_2_4_2","first-page":"133","article-title":"13 questions about universal logic","volume":"35","author":"B\u00e9ziau J-Y","year":"2006","journal-title":"Bull Sect Log"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0346-0145-0"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Birkhoff G (1935) On the structure of abstract algebras. In: Mathematical proceedings of the Cambridge philosophical society vol 31 pp 433\u2013454","DOI":"10.1017\/S0305004100013463"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.339"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Blackburn P Marx M (2002) Tableaux for quantified hybrid logic. In: Egly U Ferm\u00fcller CG (eds) Automated reasoning with analytic tableaux and related methods international conference TABLEAUX 2002 Copenhagen Denmark July 30\u2013August 1 2002 proceedings volume 2381 of lecture notes in computer science. Springer pp 38\u201352","DOI":"10.1007\/3-540-45616-3_4"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bra\u00fcner T (2011) Hybrid logic and its Proof-Theory applied logic series vol 37. Springer Berlin","DOI":"10.1007\/978-94-007-0002-4"},{"key":"e_1_2_1_2_10_2","unstructured":"Carnielli W Coniglio M Gabbay DM Gouveia P Sernadas C (2008) Analysis and synthesis of logics\u2014how To cut and paste reasoning systems. Applied logic series. Springer Berlin"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11787-008-0035-1"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00361-9"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/2370945.2370950"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.01.005"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi082"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1481586"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exr007"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Diaconescu R (2016) Implicit kripke semantics and ultraproducts in stratified Institutions. J Log Comput. doi:10.1093\/logcom\/exw018","DOI":"10.1093\/logcom\/exw018"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/ext016"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000383"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00156915"},{"issue":"16","key":"e_1_2_1_2_22_2","first-page":"2204","article-title":"Constructor-based logics.","volume":"18","author":"G\u0103in\u0103 D","year":"2012","journal-title":"J UCS"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq012"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.12.002"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"G\u0103in\u0103 D (2015) Downward L\u00f6wenheim-Skolem theorem and interpolation in logics with constructors. J Log Comput. doi:10.1093\/logcom\/exv018","DOI":"10.1093\/logcom\/exv018"},{"key":"e_1_2_1_2_26_2","unstructured":"G\u0103in\u0103 D (2015) Foundations of logic programming in hybrid logics with user-defined sharing. TheoretComput Sci (submitted)"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"G\u0103in\u0103 D (2015) Foundations of logic programming in hybridised logics. In: Codescu M Diaconescu R \u0162u\u0163u I (eds) Recent trends in algebraic development techniques\u201422nd international workshop WADT 2014 Sinaia Romania September 4\u20137 2014 proceedings volume 9463 of lecture notes in computer science. Springer pp 69\u201389","DOI":"10.1007\/978-3-319-28114-8_5"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"issue":"3","key":"e_1_2_1_2_29_2","first-page":"307","article-title":"Completeness of many-sorted equational logic","volume":"11","author":"Goguen J","year":"1985","journal-title":"Houst J Math"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_2_1_2_31_2","unstructured":"Goguen J (1994) Theorem proving and algebra. https:\/\/cseweb.ucsd.edu\/~goguen\/pubs\/tp.html"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"e_1_2_1_2_33_2","unstructured":"Madeira A (2013) Foundations and techniques for software reconfigurability. Ph.D. thesis Universidades do Minho Aveiro and Porto Joint MAP-i Doctoral Programme"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Meseguer J (1989) General logics. In: Ebbinghaus H-D Fernandez-Prida J Garrido M Lascar D Rodriguez Artalejo M (eds) Logic Colloquium \u201987. Studies in logic and the foundations of mathematics vol 129 North Holland pp 275\u2013329","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0327-6"},{"key":"e_1_2_1_2_36_2","unstructured":"Martins MA Madeira A Diaconescu R Barbosa LS (2011) Hybridization of institutions. In: Corradini A Klin B C\u00eerstea C (eds) Algebra and coalgebra in computer science\u20144th international conference CALCO 2011 Winchester UK August 30\u2014September 2 2011 Proceedings volume 6859 of lecture notes in computer science. Springer pp 283\u2013297"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.03.001"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90026-X"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Petria M (2007) An institutional version of G\u00f6del\u2019s completeness theorem. In: Mossakowski T Montanari U Haveraaen M (eds) Algebra and coalgebra in computer science second international conference CALCO 2007 Bergen Norway August 20\u201324 2007 proceedings volume 4624 of lecture notes in computer science Springer. pp 409\u2013424","DOI":"10.1007\/978-3-540-73859-6_28"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, present and future. Oxford books","author":"Prior A","year":"1967"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzp085"},{"issue":"1","key":"e_1_2_1_2_42_2","first-page":"74","article-title":"An overview on software reconfiguration.","volume":"1","author":"Szepesia R","year":"2011","journal-title":"Theory Appl Math Comput Sci"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Tarlecki A (1986) Bits and pieces of the theory of institutions. In: Pitt D Abramsky S Poign\u00e9 A Rydeheard D (eds) Proceedings summer workshop on category theory and computer programming lecture notes in computer science vol 240. Springer pp 334\u2013360","DOI":"10.1007\/3-540-17162-2_132"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90057-7"},{"key":"e_1_2_1_2_45_2","unstructured":"\u0162u\u0163u I Fiadeiro JL (2015) Revisiting the Institutional approach to Herbrand\u2019s theorem. In: Moss LS Sobocinski P (eds) 6th conference on Algebra and Coalgebra in computer science CALCO 2015 June 24\u201326 2015 Nijmegen The Netherlands volume 35 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Wadern"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0414-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0414-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0414-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0414-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:19Z","timestamp":1641538459000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0414-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":45,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-016-0414-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0414-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}