000			01973nam a2200301Ia 4500
000			02604nam a22003375i 4500
001			978-3-031-24934-1
003			DE-He213
005			20240319120856.0
007			cr nn 008mamaa
008			230411s2023 sz | s |||| 0|eng d
020			_a9783031249341 _9978-3-031-24934-1
082			_a4.0151
100			_aSchreiner, Wolfgang. _931294
245			_aConcrete Abstractions _cby Wolfgang Schreiner. _h[electronic resource] :
250			_a1st ed. 2023.
260			_aCham _bSpringer International Publishing _c2023
300			_aXII, 271 p. 79 illus., 53 illus. in color. _bonline resource.
520			_aThis book demonstrates how to formally model various mathematical domains (including algorithms operating in these domains) in a way that makes them amenable to a fully automatic analysis by computer software. The presented domains are typically investigated in discrete mathematics, logic, algebra, and computer science; they are modeled in a formal language based on first-order logic which is sufficiently rich to express the core entities in whose correctness we are interested: mathematical theorems and algorithmic specifications. This formal language is the language of RISCAL, a "mathematical model checker" by which the validity of all formulas and the correctness of all algorithms can be automatically decided. The RISCAL software is freely available; all formal contents presented in the book are given in the form of specification files by which the reader may interact with the software while studying the corresponding book material.
650			_aComputational Mathematics and Numerical Analysis. _931295
650			_aComputer science _931296
650			_aMathematical Logic and Foundations. _931297
650			_aMathematical logic. _931298
650			_aMathematics _931299
650			_aMathematics of Computing. _931300
856			_uhttps://doi.org/10.1007/978-3-031-24934-1
942			_cEBK _2ddc
999			_c15199 _d15199