{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:32:30Z","timestamp":1761597150362},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10472-009-9151-8","type":"journal-article","created":{"date-parts":[[2009,7,3]],"date-time":"2009-07-03T06:45:12Z","timestamp":1246603512000},"page":"35-62","source":"Crossref","is-referenced-by-count":8,"title":["Automated verification of refinement laws"],"prefix":"10.1007","volume":"55","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"}]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,7,4]]},"reference":[{"issue":"6","key":"9151_CR1","doi-asserted-by":"crossref","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 45(6), 1007\u20131049 (1998)","journal-title":"J. ACM"},{"key":"9151_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/3-540-51285-3_42","volume-title":"Parallel Architectures and Languages Europe","author":"R-J Back","year":"1989","unstructured":"Back, R.-J.: A method for refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syr, J.-C. (eds.) Parallel Architectures and Languages Europe. Lecture Notes in Computer Science, vol. 366, pp. 199\u2013216. Springer, New York (1989)"},{"key":"9151_CR3","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)"},{"issue":"4","key":"9151_CR4","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s002360050163","volume":"36","author":"R-J Back","year":"1999","unstructured":"Back, R.-J., von Wright, J.: Reasoning algebraically about loops. Acta Inform. 36(4), 295\u2013334 (1999)","journal-title":"Acta Inform."},{"key":"9151_CR5","unstructured":"Claessen, K.: Equinox, A New Theorem Prover for Full First-Order Logic with Equality (2005)"},{"key":"9151_CR6","unstructured":"Cohen, E.: Omega algebra: the good, the bad, and the ugly. In: Backhouse, R., Kozen, D., M\u00f6ller, B. (eds.) Applications of Kleene Algebra. Report of the Dagstuhl Seminar 01081, p. 5 (2001)"},{"key":"9151_CR7","series-title":"Lecture Notes in Artificial Intelligence","first-page":"148","volume-title":"Lecture Notes in Artificial Intelligence","author":"E Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. In: Konev, B., Wolter, F. (eds.) Frontiers of Combining Systems, 6th International Symposium. Lecture Notes in Artificial Intelligence, vol. 4720, pp. 148\u2013162. Springer, New York (2007)"},{"key":"9151_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Proceedings of the 3rd International Joint Conference on Automated Reasoning","author":"H Nivelle de","year":"2006","unstructured":"de\u00a0Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, vol. 4130, pp. 303\u2013317. Springer, New York (2006)"},{"key":"9151_CR9","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W-P Roever de","year":"2001","unstructured":"de\u00a0Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (2001)"},{"key":"9151_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/978-3-540-79980-1_25","volume-title":"Algebraic Methodology and Software Technology (AMAST 2008)","author":"J Desharnais","year":"2008","unstructured":"Desharnais, J., Struth, G.: Domain axioms for a family of near-semirings. In: Meserguer, J., Ro\u015fu, G. (eds.) Algebraic Methodology and Software Technology (AMAST 2008). Lecture Notes in Computer Science, vol. 5140, pp. 330\u2013345. Springer, New York (2008)"},{"key":"9151_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1007\/978-3-540-70594-9_19","volume-title":"Mathematics of Program Construction (MPC 2008)","author":"J Desharnais","year":"2008","unstructured":"Desharnais, J., Struth, G.: Modal semirings revisited. In: Audebaud, P., Paulin-Mohrig, C. (eds.) Mathematics of Program Construction (MPC 2008). Lecture Notes in Computer Science, vol. 5133, pp. 360\u2013387. Springer, New York (2008)"},{"key":"9151_CR12","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.entcs.2004.08.049","volume":"127","author":"M Ebert","year":"2005","unstructured":"Ebert, M., Struth, G.: Diagram chase in relational system development. Electr. Notes Theor. Comp. Sci. 127, 87\u2013105 (2005)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"9151_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-540-78913-0_15","volume-title":"Relations and Kleene Algebra in Computer Science","author":"P H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P.: Automated reasoning for hybrid systems\u2014two case studies. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relations and Kleene Algebra in Computer Science. Lecture Notes in Computer Science, vol. 4988, pp. 191\u2013205. Springer, New York (2008)"},{"key":"9151_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction (CADE 21)","author":"P H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) Automated Deduction (CADE 21). Lecture Notes in Artificial Intelligence, vol. 4603, pp. 279\u2013294. Springer, New York (2007)"},{"key":"9151_CR15","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/j.entcs.2008.02.021","volume":"201","author":"P H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Can refinement be automated? Electr. Notes Theor. Comp. Sci. 201, 197\u2013222 (2007)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"9151_CR16","unstructured":"H\u00f6fner, P., Struth, G.: Algebraic reasoning with Prover9 (proof database). http:\/\/www.dcs.shef.ac.uk\/~georg\/ka (2008)"},{"key":"9151_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Deduction (IJCAR 2008)","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.) Automated Deduction (IJCAR 2008). Lecture Notes in Computer Science, vol. 5196, pp. 50\u201366. Springer, New York (2008)"},{"key":"9151_CR18","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di\u00a0Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics, Number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"9151_CR19","unstructured":"Korovin, K.: Implementing an instantiation-based theorem prover for first-order logic. In: Benzm\u00fcller, C., Fischer, B., Sutcliffe, G. (eds.) Proceedings of the 6th International Workshop on the Implementation of Logics, Number 212 in CEUR Workshop Proceedings, pp. 63\u201363 (2006)"},{"issue":"2","key":"9151_CR20","doi-asserted-by":"crossref","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. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"key":"9151_CR21","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Otter 3.3 reference manual. Technical Report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne (2003)","DOI":"10.2172\/822573"},{"key":"9151_CR22","unstructured":"McCune, W.W.: Prover9 and Mace4. http:\/\/www.cs.unm.edu\/~mccune\/prover9 (2008). Accessed 10 September 2008"},{"issue":"1","key":"9151_CR23","first-page":"90","volume":"76","author":"AK McIver","year":"2008","unstructured":"McIver, A.K., Gonzalia, C., Cohen, E., Morgan, C.C.: Using probabilistic Kleene algebra pKA for protocol verification. JLAP 76(1), 90\u2013111 (2008)","journal-title":"JLAP"},{"issue":"1\u20132","key":"9151_CR24","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: LeanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003)","journal-title":"J. Symb. Comput."},{"issue":"2\u20133","key":"9151_CR25","first-page":"79","volume":"15","author":"FJ Pelletier","year":"2002","unstructured":"Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The development of CASC. AI Commun. 15(2\u20133), 79\u201390 (2002)","journal-title":"AI Commun."},{"key":"9151_CR26","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/LICS.2004.1319598","volume-title":"LICS \u201904: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS \u201904: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32\u201341. IEEE Computer Society, Piscataway (2004)"},{"issue":"6","key":"9151_CR27","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"S Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. Trends and controversies. IEEE Intell. Syst. Mag. 21(6), 71\u201381 (2006)","journal-title":"IEEE Intell. Syst. Mag."},{"issue":"2\u20133","key":"9151_CR28","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"2\u20133","key":"9151_CR29","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E: a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9151_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/3-540-45127-7_22","volume-title":"Rewriting Techniques and Applications, 12th International Conference","author":"G Struth","year":"2001","unstructured":"Struth, G.: Deriving focused calculi for transitive relations. In: Middeldorp, A. (ed.) Rewriting Techniques and Applications, 12th International Conference. Lecture Notes in Computer Science, vol. 2051, pp. 291\u2013305. Springer, New York (2001)"},{"issue":"2","key":"9151_CR31","first-page":"239","volume":"66","author":"G Struth","year":"2006","unstructured":"Struth, G.: Abstract abstract reduction. JLAP 66(2), 239\u2013270 (2006)","journal-title":"JLAP"},{"key":"9151_CR32","unstructured":"Struth, G.: Reasoning automatically about termination and refinement. In: Ranise, S. (ed.) 6th International Workshop on First-Order Theorem Proving. Technical Report ULCS-07-018, Department of Computer Science, pp. 36\u201351. University of Liverpool (2007)"},{"key":"9151_CR33","first-page":"81","volume":"214C","author":"G Struth","year":"2008","unstructured":"Struth, G.: Modal tools for separation and refinement. Theor. Comp. Sci. 214C, 81\u2013101 (2008) (electronic notes)","journal-title":"Theor. Comp. Sci."},{"issue":"6","key":"9151_CR34","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic derivation verification. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"1","key":"9151_CR35","first-page":"71","volume":"21","author":"G Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 automated theorem proving competition. AI Commun. 21(1), 71\u201382 (2008)","journal-title":"AI Commun."},{"key":"9151_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Proceedings of the 21st International Conference on Automated Deduction","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS\u2014a semantic relevance axiom selection system. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 4603, pp. 295\u2013310. Springer, New York (2007)"},{"issue":"1","key":"9151_CR37","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"issue":"2","key":"9151_CR38","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9151_CR39","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001)","journal-title":"Artif. Intell."},{"key":"9151_CR40","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"Terese (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"9151_CR41","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 45\u201358 (2007)"},{"key":"9151_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-45442-X_14","volume-title":"Mathematics of Program Construction","author":"J Wright von","year":"2002","unstructured":"von Wright, J.: From Kleene algebra to refinement algebra. In: Boiten, E.A., M\u00f6ller, B. (eds.) Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 2386, pp. 233\u2013262. Springer, New York (2002)"},{"issue":"1\u20132","key":"9151_CR43","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","volume":"51","author":"J Wright von","year":"2004","unstructured":"von Wright, J.: Towards a refinement algebra. Sci. Comput. Program. 51(1\u20132), 23\u201345 (2004)","journal-title":"Sci. Comput. Program."},{"key":"9151_CR44","series-title":"Lecture Notes in Artificial Intelligence","first-page":"141","volume-title":"Proceedings of the 13th International Conference on Automated Deduction","author":"C Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: SPASS and FLOTTER. In: McRobbie, M., Slaney, J.K. (eds.) Proceedings of the 13th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1104, pp. 141\u2013145. Springer, New York (1996)"},{"key":"9151_CR45","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Proceedings of the 21st International Conference on Automated Deduction","author":"C Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: SPASS version 3.0. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 4603, pp. 514\u2013520. Springer, New York (2007)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9151-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-009-9151-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9151-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T00:43:32Z","timestamp":1710463412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-009-9151-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":45,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["9151"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9151-8","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}