{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T17:31:28Z","timestamp":1777915888299,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540651413","type":"print"},{"value":"9783540495451","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49545-2_18","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T18:41:28Z","timestamp":1186425688000},"page":"264-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Mechanised Proof System for Relation Algebra Using Display Logic"],"prefix":"10.1007","author":[{"given":"Jeremy E.","family":"Dawson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,2,26]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N. D. Belnap","year":"1982","unstructured":"Nuel D. Belnap, Display Logic, Journal of Philosophical Logic 11 (1982), 375\u2013417.","journal-title":"Journal of Philosophical Logic"},{"key":"18_CR2","unstructured":"Rudolf Berghammer & Claudia Hattensperger, Computer-Aided Manipulation of Relational Expressions and Formulae Using RALF, preprint."},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1017\/S0305004100013463","volume":"31","author":"G. Birkhoff","year":"1935","unstructured":"Garrett Birkhoff, On the Structure of Abstract Algebras, Proc. Cambridge Phil. Soc. 31 (1935), 433\u2013454.","journal-title":"Proc. Cambridge Phil. Soc."},{"issue":"2","key":"18_CR4","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0364-0213(85)80014-8","volume":"9","author":"R.J. Brachman","year":"1985","unstructured":"R.J. Brachman & J.G. Schmolze, An overview of the KL-ONE knowledge representation system, Cognitive Science 9(2) (1985), 171\u2013216.","journal-title":"Cognitive Science"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF01215410","volume":"6","author":"C. Brink","year":"1994","unstructured":"Chris Brink, Katarina Britz & Renate A. Schmidt, Peirce Algebras, Formal Aspects of Computing 6 (1994), 339\u2013358.","journal-title":"Peirce Algebras, Formal Aspects of Computing"},{"key":"18_CR6","first-page":"341","volume":"I","author":"L. H. Chin","year":"1943","unstructured":"Louise H. Chin & Alfred Tarski, Distributive and Modular Laws in the Arithmetic of Relation Algebras, University of California Publications in Mathematics, New Series, I (1943\u20131951), 341\u2013384.","journal-title":"Distributive and Modular Laws in the Arithmetic of Relation Algebras"},{"key":"18_CR7","unstructured":"Jeremy E. Dawson, Mechanised Proof Systems for Relation Algebras, Grad. Dip. Sci. sub-thesis, Dept of Computer Science, Australian National University. Available at http:\/\/arp.anu.edu.au:80\/~jeremy\/thesis.dvi"},{"key":"18_CR8","unstructured":"Jeremy E. Dawson, Simulating Term-Rewriting in LPF and in Display Logic, submitted. Available at http:\/\/arp.anu.edu.au:80\/~jeremy\/rewr\/rewr.dvi"},{"key":"18_CR9","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J. H. Gallier","year":"1986","unstructured":"Jean H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper & Row, New York, 1986."},{"key":"18_CR10","unstructured":"Lev Gordeev, personal communication."},{"key":"18_CR11","unstructured":"Rajeev Gor\u00e9, Intuitionistic Logic Redisplayed, Automated Reasoning Project TRARP-1-95, ANU, 1995."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-63172-0_40","volume-title":"Cut-free Display Calculi for Relation Algebras, Computer Science Logic","author":"R. Gor\u00e9","year":"1997","unstructured":"Rajeev Gor\u00e9, Cut-free Display Calculi for Relation Algebras, Computer Science Logic, Lecture Notes in Computer Science 1249 (1997), 198\u2013210. (or see http:\/\/arp.anu.edu.au\/~rpg\/publications.html )."},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1093\/comjnl\/39.4.291","volume":"39","author":"J. Grundy","year":"1996","unstructured":"Jim Grundy, Transformational Hierarchical Reasoning, The Computer Journal 39 (1996), 291\u2013302.","journal-title":"The Computer Journal"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Huet & Derek C. Oppen, Equations and Rewrite Rules \u2014 A Survey, in Formal Languages: Perspectives and Open Problems, R.V. Book (ed), Academic Press (1980), 349\u2013405.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"18_CR15","first-page":"73","volume":"25","author":"R. D. Maddux","year":"1983","unstructured":"Roger D. Maddux, A Sequent Calculus for Relation Algebras, Annals of Pure and Applied Logic 25 (1983), 73\u2013101.","journal-title":"A Sequent Calculus for Relation Algebras, Annals of Pure and Applied Logic"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/BF00370681","volume":"50","author":"R. D. Maddux","year":"1991","unstructured":"Roger D. Maddux, The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations, Studia Logica 50 (1991), 421\u2013455.","journal-title":"Studia Logica"},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/3-540-63104-6_36","volume-title":"Proceedings of CADE-14","author":"D. Oheimb von","year":"1997","unstructured":"David von Oheimb & Thomas F. Gritzner, RALL: Machine-supported proofs for Relation Algebra, Proceedings of CADE-14, Lecture Notes in Computer Science 1249 (1997), 380\u2013394."},{"key":"18_CR18","unstructured":"Lawrence C. Paulson, The Isabelle Reference Manual, Computer Laboratory, University of Cambridge, 1995."},{"key":"18_CR19","unstructured":"Lawrence C. Paulson, Isabelle\u2019s Object-Logics, Computer Laboratory, University of Cambridge, 1995."},{"key":"18_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P. J. Robinson","year":"1993","unstructured":"Peter J. Robinson & John Staples, Formalizing a Hierarchical Structure of Practical Mathematical Reasoning, J. Logic & Computation, 3 (1993), 47\u201361.","journal-title":"J. Logic & Computation"},{"key":"18_CR21","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H. Wansing","year":"1994","unstructured":"Heinrich Wansing, Sequent Calculi for Normal Modal Propositional Logics, Journal of Logic and Computation 4 (1994), 124\u2013142.","journal-title":"Journal of Logic and Computation"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49545-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T17:10:05Z","timestamp":1587834605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49545-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651413","9783540495451"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-49545-2_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"26 February 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}