{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:49Z","timestamp":1762458649918},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_5","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"50-66","source":"Crossref","is-referenced-by-count":16,"title":["On Automating the Calculus of Relations"],"prefix":"10.1007","author":[{"given":"Peter","family":"H\u00f6fner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"http:\/\/www.dcs.shef.ac.uk\/~georg\/ka"},{"key":"5_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"issue":"6","key":"5_CR3","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM\u00a045(6), 1007\u20131049 (1998)","journal-title":"J. ACM"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/11555964_4","volume-title":"Computer Algebra in Scientific Computing","author":"R. Berghammer","year":"2005","unstructured":"Berghammer, R., Neumann, F.: An OBDD-based computer algebra system for relations. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2005. LNCS, vol.\u00a03718, pp. 40\u201351. Springer, Heidelberg (2005)"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(86)90172-6","volume":"43","author":"R. Berghammer","year":"1986","unstructured":"Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theoretical Computer Science\u00a043, 123\u2013147 (1986)","journal-title":"Theoretical Computer Science"},{"key":"5_CR6","volume-title":"Algebra of Programming","author":"R. Bird","year":"1996","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"5_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"key":"5_CR8","unstructured":"Dang, H.-H., H\u00f6fner, P.: First-order theorem prover evaluation w.r.t. relation- and Kleene algebra. In: R.\u00a0Berghammer, B.\u00a0M\u00f6ller, and G.\u00a0Struth, editors, RelMiCS10\/AKA5 - PhD Programme, Technical Report 2008-04, University of Augsburg, pp. 48\u201352 (2008)"},{"key":"5_CR9","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W.-P. Roever de","year":"2001","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (2001)"},{"key":"5_CR10","series-title":"Lecture Notes in Artificial Intelligence","first-page":"1","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Formisano","year":"2005","unstructured":"Formisano, A., Omodeo, E.G., Or\u0142owska, E.: A Prolog tool for relational translations of modal logics: A front-end for relational proof systems. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 1\u201311. Springer, Heidelberg (2005)"},{"key":"5_CR11","volume-title":"Cylindric Algebras, Part I","author":"L. Henkin","year":"1971","unstructured":"Henkin, L., Monk, D.J., Tarski, A.: Cylindric Algebras, Part I. North-Holland, Amsterdam (1971)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"557","DOI":"10.2307\/1989783","volume":"35","author":"E.V. Huntington","year":"1933","unstructured":"Huntington, E.V.: Boolean algebra. A correction. Trans. AMS\u00a035, 557\u2013558 (1933)","journal-title":"Trans. AMS"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"274","DOI":"10.2307\/1989325","volume":"35","author":"E.V. Huntington","year":"1933","unstructured":"Huntington, E.V.: New sets of independent postulates for the algebra of logic. Trans. AMS\u00a035, 274\u2013304 (1933)","journal-title":"Trans. AMS"},{"key":"5_CR14","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"891","DOI":"10.2307\/2372123","volume":"74","author":"B. J\u00f3nsson","year":"1951","unstructured":"J\u00f3nsson, B., Tarski, A.: Boolean algebras with operators I. American J. Mathematics\u00a074, 891\u2013939 (1951)","journal-title":"American J. Mathematics"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","first-page":"179","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 179\u2013190. Springer, Heidelberg (2004)"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1023\/A:1020572931854","volume":"71","author":"W. MacCaull","year":"2002","unstructured":"MacCaull, W., Orlowska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica\u00a071(3), 389\u2013414 (2002)","journal-title":"Studia Logica"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0168-0072(83)90055-6","volume":"25","author":"R. Maddux","year":"1983","unstructured":"Maddux, R.: A sequent calculus for relation algebras. Annals of Pure and Applied Logic\u00a025, 73\u2013101 (1983)","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR19","volume-title":"Relation Algebras","author":"R. Maddux","year":"2006","unstructured":"Maddux, R.: Relation Algebras. Elsevier, Amsterdam (2006)"},{"issue":"1&2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(95)00082-8","volume":"160","author":"R.D. Maddux","year":"1996","unstructured":"Maddux, R.D.: Relation-algebraic semantics. Theoretical Computer Science\u00a0160(1&2), 1\u201385 (1996)","journal-title":"Theoretical Computer Science"},{"key":"5_CR21","unstructured":"McCune, W.: Prover9 and Mace4, \n                    \n                      http:\/\/www.cs.unm.edu\/~mccune\/prover9"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"J. Automated Reasoning"},{"key":"5_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-77968-8","volume-title":"Relations and Graphs: Discrete Mathematics for Computer Scientists","author":"G. Schmidt","year":"1993","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and Graphs: Discrete Mathematics for Computer Scientists. Springer, Heidelberg (1993)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/10721959_13","volume-title":"Automated Deduction - CADE-17","author":"C. Sinz","year":"2000","unstructured":"Sinz, C.: System description: ARA \u2014 An automated theorem prover for relation algebras. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 177\u2013182. Springer, Heidelberg (2000)"},{"key":"5_CR25","volume-title":"Understanding Z","author":"J.M. Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z. Cambridge University Press, Cambridge (1988)"},{"issue":"2","key":"5_CR26","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J. Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"J. Automated Reasoning"},{"issue":"1\u20132","key":"5_CR27","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artificial Intelligence\u00a0131(1\u20132), 39\u201354 (2001)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"5_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A. Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. Journal of Symbolic Logic\u00a06(3), 73\u201389 (1941)","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.R.: A Formalization of Set Theory Without Variables. American Mathematical Society (1987)","DOI":"10.1090\/coll\/041"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/3-540-63104-6_36","volume-title":"Automated Deduction - CADE-14","author":"D. Oheimb von","year":"1997","unstructured":"von Oheimb, D., Gritzner, T.F.: Rall: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 380\u2013394. Springer, Heidelberg (1997)"},{"key":"5_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:35Z","timestamp":1620016595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}