{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:10:01Z","timestamp":1748581801379,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319231648"},{"type":"electronic","value":"9783319231655"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_27","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"580-597","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Formal System of Dijkstra and Scholten"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"27_CR1","volume-title":"Program Construction: Calculating Implementations from Specifications","author":"R Backhouse","year":"2003","unstructured":"Backhouse, R.: Program Construction: Calculating Implementations from Specifications. Wiley, New York (2003)"},{"issue":"12","key":"27_CR2","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1007\/s002360050150","volume":"35","author":"L Bijlsma","year":"1998","unstructured":"Bijlsma, L., Nederpelt, R.: Dijkstra-Scholten predicate calculus: concepts and misconceptions. Acta Informatica 35(12), 1007\u20131036 (1998)","journal-title":"Acta Informatica"},{"issue":"4","key":"27_CR3","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1215\/00294527-2008-017","volume":"49","author":"J Boh\u00f3rquez","year":"2008","unstructured":"Boh\u00f3rquez, J.: Intuitionistic logic according to Dijkstra\u2019s calculus of equational deduction. Notre Dame J. Formal Log. 49(4), 361\u2013384 (2008)","journal-title":"Notre Dame J. Formal Log."},{"issue":"5","key":"27_CR4","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/s00165-009-0137-4","volume":"22","author":"J Boh\u00f3rquez","year":"2010","unstructured":"Boh\u00f3rquez, J.: An elementary and unified approach to program correctness. Formal Aspects Comput. 22(5), 611\u2013627 (2010)","journal-title":"Formal Aspects Comput."},{"issue":"1\u20133","key":"27_CR5","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoret. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"27_CR6","series-title":"Prentice-Hall Series in Automatic Computation","volume-title":"A Discipline of Programming","author":"E Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Upper Saddle River (1976)"},{"key":"27_CR7","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E Dijkstra","year":"1990","unstructured":"Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, New York (1990)"},{"issue":"7","key":"27_CR8","first-page":"816","volume":"81","author":"J Meseguer","year":"2011","unstructured":"Meseguer, J., Dur\u00e1n, F.: On the and coherence properties of conditional rewrite theories. J. Log. Algebraic Program. 81(7), 816\u2013850 (2011)","journal-title":"J. Log. Algebraic Program."},{"key":"27_CR9","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A Logical Approach to Discrete Math","author":"D Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, New Yok (1993)"},{"issue":"3","key":"27_CR10","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/0020-0190(94)00198-8","volume":"53","author":"D Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145\u2013152 (1995)","journal-title":"Inf. Process. Lett."},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Grundy, J.: Window inference in the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA, pp. 177\u2013189. IEEE Computer Society (1992)","DOI":"10.1109\/HOL.1991.596285"},{"issue":"10","key":"27_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"27_CR13","volume-title":"An Introduction to Mathematical Logic","author":"R Hodel","year":"2013","unstructured":"Hodel, R.: An Introduction to Mathematical Logic. Dover Books on Mathematics Series. Dover Publications Incorporated, New York (2013)"},{"key":"27_CR14","unstructured":"Hsiang, J.: Topics in automated theorem proving and program generation. Ph.D. thesis, University of Illinois at Urbana-Champaign, Computer Science Department (1982)"},{"issue":"1\u20133","key":"27_CR15","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0168-0072(01)00059-8","volume":"113","author":"V Lifschitz","year":"2001","unstructured":"Lifschitz, V.: On calculational proofs. Annals Pure Appl. Log. 113(1\u20133), 207\u2013224 (2001)","journal-title":"Annals Pure Appl. Log."},{"issue":"3","key":"27_CR16","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/j.entcs.2009.05.021","volume":"238","author":"S Lucas","year":"2009","unstructured":"Lucas, S., Meseguer, J.: Operational termination of membership equational programs: the order-sorted way. Electron. Notes Theo. Comput. Sci. 238(3), 207\u2013225 (2009)","journal-title":"Electron. Notes Theo. Comput. Sci."},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, Francesco (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"issue":"1\u20132","key":"27_CR18","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"Higher-Order Symbolic Comput."},{"key":"27_CR19","unstructured":"Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical report 2007\u20132818, University of Illinois at Urbana-Champaign (2007)"},{"key":"27_CR20","unstructured":"Rocha, C., Meseguer, J.: Theorem proving modulo based on Boolean equational procedures. Technical report 2007\u20132922, University of Illinois at Urbana-Champaign (2007)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78913-0_25","volume-title":"Relations and Kleene Algebra in Computer Science","author":"C Rocha","year":"2008","unstructured":"Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS\/AKA 2008. LNCS, vol. 4988, pp. 337\u2013351. Springer, Heidelberg (2008)"},{"key":"27_CR22","volume-title":"Deduction Systems (Texts in Computer Science)","author":"R Socher-Ambrosius","year":"1996","unstructured":"Socher-Ambrosius, R., Johann, P.: Deduction Systems (Texts in Computer Science). Springer-Verlag, New York (1996)"},{"key":"27_CR23","series-title":"International Series in Pure and Applied Mathematics","volume-title":"Introduction to Topology and Modern Analysis","author":"G Simmons","year":"1963","unstructured":"Simmons, G.: Introduction to Topology and Modern Analysis. International Series in Pure and Applied Mathematics. Krieger Publishing Company, Malabar (1963)"},{"issue":"4","key":"27_CR24","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1093\/logcom\/11.4.623","volume":"11","author":"G Tourlakis","year":"2001","unstructured":"Tourlakis, G.: On the soundness and completeness of equational predicate logics. J. Log. Comput. 11(4), 623\u2013653 (2001)","journal-title":"J. Log. Comput."},{"key":"27_CR25","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoret. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:39:55Z","timestamp":1748579995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}