{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:46Z","timestamp":1725573886403},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_31","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:35:57Z","timestamp":1294396557000},"page":"541-559","source":"Crossref","is-referenced-by-count":3,"title":["A Calculus for Set-Based Program Development"],"prefix":"10.1007","author":[{"given":"Georg","family":"Struth","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"publisher","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":"3","key":"31_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"J. Logic and Computation"},{"key":"31_CR3","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1109\/LICS.1994.316051","volume-title":"Ninth Annual IEEE Symposium on Logic in Computer Science","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 384\u2013393. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"31_CR4","series-title":"Colloquium Publications","volume-title":"Lattice Theory","author":"G. Birkhoff","year":"1984","unstructured":"Birkhoff, G.: Lattice Theory. Colloquium Publications, vol.\u00a025. American Mathematical Society, Providence (1984) (reprint)"},{"key":"31_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1090\/S0002-9947-1945-0012263-6","volume":"57","author":"R.P. Dilworth","year":"1945","unstructured":"Dilworth, R.P.: Lattices with unique complements. Trans. Amer. Math. Soc.\u00a057, 123\u2013154 (1945)","journal-title":"Trans. Amer. Math. Soc."},{"key":"31_CR6","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.C., van der Woude, J.: A calculation approach to mathematical induction. Theoretical Computer Science\u00a0179, 103\u2013135 (1997)","journal-title":"Theoretical Computer Science"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0105405","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Gordon","year":"1996","unstructured":"Gordon, M.: Set theory, higher-order logic or both? In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 191\u2013202. Springer, Heidelberg (1996)"},{"key":"31_CR8","doi-asserted-by":"crossref","first-page":"137","DOI":"10.4064\/fm-38-1-137-152","volume":"38","author":"A. Grzegorczyk","year":"1951","unstructured":"Grzegorczyk, A.: Undecidability of some topological theories. Fund. Math.\u00a038, 137\u2013152 (1951)","journal-title":"Fund. Math."},{"key":"31_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86524-4","volume-title":"Einf\u00fchrung in die Verbandstheorie","author":"H. Hermes","year":"1967","unstructured":"Hermes, H.: Einf\u00fchrung in die Verbandstheorie. Springer, Heidelberg (1967)"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-52885-7_88","volume-title":"10th International Conference on Automated Deduction","author":"L. Hines","year":"1990","unstructured":"Hines, L.: Str+\u2009.ve\u2286: The Str+\u2009.ve-based Subset Prover. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 193\u2013206. Springer, Heidelberg (1990)"},{"issue":"3","key":"31_CR11","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0020-0190(94)00205-D","volume":"53","author":"C.A.R. Hoare","year":"1995","unstructured":"Hoare, C.A.R., von Karger, B.: Sequential calculus. Information Processing Letters\u00a053(3), 123\u2013130 (1995)","journal-title":"Information Processing Letters"},{"key":"31_CR12","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(80)90048-1","volume":"10","author":"D. Kozen","year":"1980","unstructured":"Kozen, D.: Complexity of Boolean algebras. Theoretical Computer Science\u00a010, 221\u2013247 (1980)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"31_CR13","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. Transation on Programming Languages and Systems\u00a019(3), 427\u2013443 (1997)","journal-title":"Transation on Programming Languages and Systems"},{"key":"31_CR14","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Automated Reasoning\u00a011, 353\u2013389 (1993)","journal-title":"From foundations to functions. J. Automated Reasoning"},{"key":"31_CR15","first-page":"91","volume":"8","author":"A. Quaife","year":"1993","unstructured":"Quaife, A.: Automated deduction in von-Neumann-Bernays-G\u00f6del set theory. J. Automated Deduction\u00a08, 91\u2013147 (1993)","journal-title":"J. Automated Deduction"},{"key":"31_CR16","unstructured":"Rudnicki, P.: An overwiev of the MIZAR project. Technical report, Department of Computing Science, University of Alberta (1992)"},{"key":"31_CR17","volume-title":"Understanding Z","author":"J.M. Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z. Cambrigde University Press, Cambridge (1988)"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/10721975_15","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2000","unstructured":"Struth, G.: An algebra of resolution. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 214\u2013228. Springer, Heidelberg (2000)"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45127-7_22","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2001","unstructured":"Struth, G.: Deriving focused calculi for transitive relations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 291\u2013305. Springer, Heidelberg (2001)"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45610-4_7","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"2002","unstructured":"Struth, G.: Deriving focused lattice calculi. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 83\u201397. Springer, Heidelberg (2002)"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Struth, G.: A calculus for set-based program development I: Mathematical foundations. Technical Report 2003-15, Institut f\u00fcr Informatik; Universit\u00e4t Augsburg (2003)","DOI":"10.1007\/978-3-540-39893-6_31"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Struth, G.: A calculus for set-based program development II: Proof search. Technical Report 2003-16, Institut f\u00fcr Informatik; Universit\u00e4t Augsburg (2003)","DOI":"10.1007\/978-3-540-39893-6_31"},{"issue":"64","key":"31_CR23","first-page":"1192","volume":"55","author":"A. Tarski","year":"1949","unstructured":"Tarski, A.: Arithmetical classes and types of Boolean algebras. Bull. Am. Math. Soc.\u00a055(64), 1192 (1949)","journal-title":"Bull. Am. Math. Soc."},{"key":"31_CR24","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning: Classical Papers on Computational Logic","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivations in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers on Computational Logic, pp. 466\u2013483. Springer, Heidelberg (1983) (reprint)"}],"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-540-39893-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T13:43:21Z","timestamp":1559915001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}