Abstract
The standard mathematical definition of signed integers, based on set theory, is not well-adapted to the needs of computer science. For this reason, many formal specification languages and theorem provers have designed alternative definitions of signed integers based on term algebras, by extending the Peano-style construction of unsigned naturals using “zero” and “succ” to the case of signed integers. We compare the various approaches used in CADP, CASL, Coq, Isabelle/HOL, KIV, Maude, mCRL2, PSF, SMT-LIB, TLA+, etc. according to objective criteria and suggest an “optimal” definition of signed integers.
Cite
CITATION STYLE
Garavel, H. (2017). On the most suitable axiomatization of signed integers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10644 LNCS, pp. 120–134). Springer Verlag. https://doi.org/10.1007/978-3-319-72044-9_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
