{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T23:42:36Z","timestamp":1725925356819},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319720432"},{"type":"electronic","value":"9783319720449"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-72044-9_9","type":"book-chapter","created":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T14:14:43Z","timestamp":1512656083000},"page":"120-134","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Most Suitable Axiomatization of\u00a0Signed\u00a0Integers"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,8]]},"reference":[{"key":"9_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard - Version 2.5, 93 p., June 2015"},{"key":"9_CR2","unstructured":"Bergstra, J.A.: Four complete datatype defining rewrite systems for an abstract datatype of natural numbers (version 3). Report TCS1407v3, University of Amsterdam (UvA), The Netherlands, June 2014"},{"key":"9_CR3","unstructured":"Bergstra, J.A., Ponse, A.: Datatype defining rewrite systems for the ring of integers, and for natural and integer arithmetic in unary view. The Computing Research Repository (CoRR) abs\/1608.06212, August 2016. http:\/\/arxiv.org\/abs\/1608.06212"},{"key":"9_CR4","unstructured":"Bergstra, J.A., Ponse, A.: Three datatype defining rewrite systems for datatypes of integers each extending a datatype of naturals (version 3). Report TCS1409v3, University of Amsterdam (UvA), The Netherlands, February 2016. http:\/\/arxiv.org\/abs\/1406.3280"},{"key":"9_CR5","unstructured":"Berry, G.: The Esterel V5 Language Primer \u2013 Version v5_91. INRIA Sophia-Antipolis, France, June 2000"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude \u2013 A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude \u2013 A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-53904-2_100","volume-title":"Rewriting Techniques and Applications","author":"D Cohen","year":"1991","unstructured":"Cohen, D., Watson, P.: An efficient representation of arithmetic for term rewriting. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 240\u2013251. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53904-2_100"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-62950-5_64","volume-title":"Rewriting Techniques and Applications","author":"E Contejean","year":"1997","unstructured":"Contejean, E., March\u00e9, C., Rabehasaina, L.: Rewrite systems for natural, integral, and rational arithmetic. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 98\u2013112. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_64"},{"key":"9_CR9","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1 - Equations and Initial Semantics","author":"H Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1 - Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science, vol. 6. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-69962-7"},{"key":"9_CR10","unstructured":"Ernst, G., Haneberg, D., Pf\u00e4hler, J., Reif, W., Schellhorn, G., Stenzel, K., Tofan., B.: A practical course on KIV. Technical report, 152 p., Institute for Software and Systems Engineering, University of Augsburg, Germany (2015)"},{"key":"9_CR11","unstructured":"Garavel, H.: Compilation of LOTOS abstract data types. In: Vuong, S.T. (ed.) Proceedings of the 2nd International Conference on Formal Description Techniques, Vancouver B.C., Canada, FORTE 1989, pp. 147\u2013162. North-Holland, December 1989"},{"key":"9_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"J Groote","year":"2014","unstructured":"Groote, J., Mousavi, M.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)"},{"key":"9_CR13","unstructured":"Houssais, B.: The Synchronous Programming Language SIGNAL \u2013 A Tutorial. INRIA Rennes, France, September 2004"},{"key":"9_CR14","unstructured":"ISO\/IEC: LOTOS \u2013 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization \u2013 Information Processing Systems \u2013 Open Systems Interconnection, Geneva, September 1989"},{"key":"9_CR15","unstructured":"ISO\/IEC: Vienna Development Method \u2013 Specification Language \u2013 Part 1: Base Language. Internation Standard 13817-1:1996, International Organization for Standardization \u2013 Programming Languages, their Environments and System Software Interfaces, Geneva, December 1995"},{"key":"9_CR16","unstructured":"ISO\/IEC: Z Formal Specification Notation \u2013 Syntax, Type System and Semantics. International Standard 13568:2002, International Organization for Standardization \u2013 Information Technology, Geneva, July 2002"},{"key":"9_CR17","unstructured":"Kennaway, J.R.: Complete term rewrite systems for decimal arithmetic and other total recursive functions. In: Proceedings of the 2nd International Workshop on Termination, La Bresse, France, May 1995"},{"key":"9_CR18","volume-title":"Specifying Systems \u2013 The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems \u2013 The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"9_CR19","unstructured":"Larsen, P.G., Lausdahl, K., Battle, N.: VDM-10 language manual. Technical report TR-2010-06, Overture \u2013 Open-source Tools for Formal Modelling, April 2010"},{"key":"9_CR20","unstructured":"Lecomte, T.: B Language Reference Manual (Version 1.8.7). ClearSy System Engineering, Aix-en-Provence, France (2010)"},{"key":"9_CR21","unstructured":"Mauw, S., Mulder, J.: A PSF library of data types. In: van den Brand, M.G.J., van Deursen, A., Dinesh, T.B., Kamperman, J., Visser, E. (eds.) Proceedings of ASF+SDF 1995: A Workshop on Generating Tools From Algebraic Specifications, May 1995. http:\/\/ivi.fnwi.uva.nl\/tcs\/pub\/reports\/1995\/P9504\/5.html . Technical report P9504-5, Programming Research Group, University of Amsterdam, The Netherlands"},{"key":"9_CR22","series-title":"Dover Books on Mathematics Series","volume-title":"Number Systems and the Foundations of Analysis","author":"E Mendelson","year":"1973","unstructured":"Mendelson, E.: Number Systems and the Foundations of Analysis. Dover Books on Mathematics Series. Courier Corporation, Chelmsford (1973)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b96103","volume-title":"CASL Reference Manual \u2013 The Complete Documentation of the Common Algebraic Specification Language","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual \u2013 The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/b96103"},{"key":"9_CR24","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic (2016). http:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf (Early Version: Lecture Notes in Computer Science, vol. 2283, Springer, 2002)"},{"key":"9_CR25","unstructured":"Owre, S., Shankar, N.: The PVS prelude library. Technical report CSL-03-01, SRI International, Computer Science Laboratory, March 2003"},{"key":"9_CR26","unstructured":"Paulin-Mohring, C.: Basics of COQ (Sep 2011), Lecture Notes of the LASER 2011 Summer School"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Thompson, S.J.: Laws in Miranda. In: Proceedings of the ACM Conference on LISP and Functional Programming (LFP 1986), pp. 1\u201312 (1986)","DOI":"10.1145\/319838.319839"},{"key":"9_CR28","unstructured":"Isabelle\/HOL \u2013 Higher-Order Logic. University of Cambridge, Technische Universit\u00e4t M\u00fcnchen, February 2016. http:\/\/isabelle.in.tum.de\/website-Isabelle2016\/dist\/library\/HOL\/HOL\/document.pdf"},{"key":"9_CR29","unstructured":"van der Kamp, L.: A Term Rewrite System for Decimal Integer Arithmetic. Bachelor Informatica, University of Amsterdam (UvA), The Netherlands, June 2016"},{"key":"9_CR30","unstructured":"van Wamel, J.J.: A Library for PSF. Report PR9301, Programming Research Group, University of Amsterdam, The Netherlands (1993)"},{"key":"9_CR31","unstructured":"Verimag: Lustre Language Reference Manual \u2013 Versions 3, 3+, 4, 5. Grenoble, France, September 1997"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-59200-8_67","volume-title":"Rewriting Techniques and Applications","author":"HR Walters","year":"1995","unstructured":"Walters, H.R., Zantema, H.: Rewrite systems for integer arithmetic. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 324\u2013338. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59200-8_67"},{"key":"9_CR33","unstructured":"Walters, H.R.: A complete term rewriting system for decimal integer arithmetic. Technical report CS-R9435, CWI, Amsterdam, The Netherlands (1994)"},{"key":"9_CR34","unstructured":"Zantema, H.: Basic Arithmetic by Rewriting and its Complexity, Technical University of Eindhoven, The Netherlands, December 2003. http:\/\/www.win.tue.nl\/~hzantema\/aritm.pdf"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72044-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T17:02:01Z","timestamp":1570467721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72044-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319720432","9783319720449"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72044-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}