{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T06:10:18Z","timestamp":1741846218309,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642245589"},{"type":"electronic","value":"9783642245596"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24559-6_41","type":"book-chapter","created":{"date-parts":[[2011,10,21]],"date-time":"2011-10-21T15:13:17Z","timestamp":1319209997000},"page":"617-632","source":"Crossref","is-referenced-by-count":11,"title":["Automating Algebraic Methods in Isabelle"],"prefix":"10.1007","author":[{"given":"Walter","family":"Guttmann","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"41_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, Heidelberg (2009)","edition":"3"},{"key":"41_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-16780-3_76","volume-title":"8th International Conference on Automated Deduction","author":"L. Bachmair","year":"1986","unstructured":"Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 5\u201320. Springer, Heidelberg (1986)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"41_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"41_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"key":"41_CR6","volume-title":"Regular Algebra and Finite Machines","author":"J.H. Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)"},{"issue":"1","key":"41_CR7","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput.\u00a07(1), 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"issue":"4","key":"41_CR8","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic\u00a07(4), 798\u2013833 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1:1","key":"41_CR9","first-page":"1","volume":"7","author":"J. Desharnais","year":"2011","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Algebraic notions of termination. Logical Methods in Computer Science\u00a07(1:1), 1\u201329 (2011)","journal-title":"Logical Methods in Computer Science"},{"issue":"3","key":"41_CR10","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/j.scico.2010.05.007","volume":"76","author":"J. Desharnais","year":"2011","unstructured":"Desharnais, J., Struth, G.: Internal axioms for domain semirings. Sci. Comput. Program.\u00a076(3), 181\u2013203 (2011)","journal-title":"Sci. Comput. Program."},{"key":"41_CR11","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"1-2","key":"41_CR12","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos","year":"1997","unstructured":"Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. Theor. Comput. Sci.\u00a0179(1-2), 103\u2013135 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"41_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-21070-9_5","volume-title":"Relational and Algebraic Methods in Computer Science","author":"S. Foster","year":"2011","unstructured":"Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle\/HOL. In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol.\u00a06663, pp. 52\u201367. Springer, Heidelberg (2011)"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2009","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"key":"41_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"issue":"8","key":"41_CR16","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"C.A.R. Hoare","year":"1987","unstructured":"Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C.C., Roscoe, A.W., Sanders, J.W., Sorensen, I.H., Spivey, J.M., Sufrin, B.A.: Laws of programming. Commun. ACM\u00a030(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"41_CR17","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice Hall Europe (1998)","DOI":"10.1007\/BFb0002714"},{"key":"41_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"41_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Reasoning","author":"P. H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 50\u201366. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"41_CR20","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10472-009-9151-8","volume":"55","author":"P. H\u00f6fner","year":"2009","unstructured":"H\u00f6fner, P., Struth, G., Sutcliffe, G.: Automated verification of refinement laws. Annals of Mathematics and Artificial Intelligence\u00a055(1-2), 35\u201362 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"7","key":"41_CR21","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1142\/S0218196709005354","volume":"19","author":"M. Jackson","year":"2009","unstructured":"Jackson, M., Stokes, T.: Semigroups with if-then-else and halting programs. International Journal of Algebra and Computation\u00a019(7), 937\u2013961 (2009)","journal-title":"International Journal of Algebra and Computation"},{"issue":"2","key":"41_CR22","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390 (1994)","journal-title":"Information and Computation"},{"issue":"1","key":"41_CR23","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic\u00a01(1), 60\u201376 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"41_CR24","doi-asserted-by":"crossref","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning (2011), http:\/\/dx.doi.org\/10.1007\/s10817-011-9223-4","DOI":"10.1007\/s10817-011-9223-4"},{"issue":"1-2","key":"41_CR25","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. Theor. Comput. Sci.\u00a0160(1-2), 1\u201385 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"41_CR26","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","volume":"351","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: Algebras of modal operators and partial correctness. Theor. Comput. Sci.\u00a0351(2), 221\u2013239 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"41_CR27","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"41_CR28","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 3\u201313 (2010)"},{"key":"41_CR29","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph.D. thesis, TU M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24559-6_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T04:59:09Z","timestamp":1741841949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24559-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642245589","9783642245596"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24559-6_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}