{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:50:07Z","timestamp":1783684207961,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642249327","type":"print"},{"value":"9783642249334","type":"electronic"}],"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-24933-4_17","type":"book-chapter","created":{"date-parts":[[2011,10,29]],"date-time":"2011-10-29T08:11:49Z","timestamp":1319875909000},"page":"329-351","source":"Crossref","is-referenced-by-count":10,"title":["Towards a Maude Formal Environment"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9 Mar\u00eda","family":"\u00c1lvarez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"User interfaces for theorem provers, http:\/\/www.informatik.uni-bremen.de\/uitp\/"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Aspinall, D., L\u00fcth, C.: Special issue on user interfaces in theorem proving. Journal of Automated Reasoning 39(2) (2007)","DOI":"10.1007\/s10817-007-9075-0"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science\u00a0285, 187\u2013243 (2002)","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"17_CR4","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Stehr, M.O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1684\u20131703. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48118-4_39"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Hendrix, J., Lucas, S., Meseguer, J., \u00d6lveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol.\u00a04624, pp. 173\u2013178. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73859-6_12"},{"key":"17_CR7","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science\u00a012(11), 1618\u20131650 (2006)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Bevilacqua, V.: MTT: The Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 313\u2013319. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-71070-7_27"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electronic Notes in Theoretical Computer Science\u00a0248, 93\u2013113 (2009)","DOI":"10.1016\/j.entcs.2009.07.062"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 246\u2013262. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-04222-5_15"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications. In: \u00d6lveczky, P. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16310-4_6"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: \u00d6lveczky, P. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 86\u2013103. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16310-4_7"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Science of Computer Programming\u00a066(2), 125\u2013153 (2007)","DOI":"10.1016\/j.scico.2006.07.002"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming (submitted for publication, 2011)","DOI":"10.1016\/j.jlap.2012.03.012"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., \u00d6lveczky, P.C.: A guide to extending Full Maude illustrated with the implementation of Real-Time Maude. Electronic Notes in Theoretical Computer Science\u00a0238(3), 83\u2013102 (2009)","DOI":"10.1016\/j.entcs.2009.05.014"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Franssen, M., van den Brand, M.: Design of a proof repository architecture. In: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009), pp. 19\u201323. ACM (2009)","DOI":"10.1145\/1735813.1735817"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)","DOI":"10.1007\/11814771_24"},{"key":"17_CR18","unstructured":"Hemer, D., Long, G., Strooper, P.: Plug-in proof support for formal development environments. In: Proceedings of the 2005 Australasian Symposium on Theory of Computing (CATS 2005), pp. 69\u201379. Australian Computer Society, Inc. (2005)"},{"key":"17_CR19","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, University of Illinois at Urbana-Champaign (2008)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Hendrix, J., Clavel, M., Bevilacqua, V.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 165\u2013174. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-32033-3_13"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 151\u2013155. Springer, Heidelberg (2006)","DOI":"10.1007\/11814771_14"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Lucas, S.: MU-TERM: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 200\u2013209. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-25979-4_14"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of rewrite theories. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 594\u2013609. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16242-8_42"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling: Actors, Open Systems, Biological Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24933-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T19:58:57Z","timestamp":1560887937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24933-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642249327","9783642249334"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24933-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}