000 03459nam a22005415i 4500
001 978-3-031-24934-1
003 DE-He213
005 20240423125507.0
007 cr nn 008mamaa
008 230411s2023 sz | s |||| 0|eng d
020 _a9783031249341
_9978-3-031-24934-1
024 7 _a10.1007/978-3-031-24934-1
_2doi
050 4 _aQA76.9.M35
072 7 _aUYAM
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYAM
_2thema
082 0 4 _a004.0151
_223
100 1 _aSchreiner, Wolfgang.
_eauthor.
_4aut
_4http://id.loc.gov/vocabulary/relators/aut
245 1 0 _aConcrete Abstractions
_h[electronic resource] :
_bFormalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker /
_cby Wolfgang Schreiner.
250 _a1st ed. 2023.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2023.
300 _aXII, 271 p. 79 illus., 53 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTexts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,
_x2197-8409
505 0 _a1. Theories and Algorithms -- 2. Searching and Sorting -- 3. Sets, Relations, and Graphs -- 4. Propositional Logic -- 5. Big Number and Polynomial Arithmetic -- 6. Puzzles and Games -- 7. Concurrent Systems -- 8. Further Topics -- Appendices -- References -- Index.
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 0 _aComputer science
_xMathematics.
650 0 _aMathematics
_xData processing.
650 0 _aMathematical logic.
650 1 4 _aMathematics of Computing.
650 2 4 _aComputational Mathematics and Numerical Analysis.
650 2 4 _aMathematical Logic and Foundations.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031249334
776 0 8 _iPrinted edition:
_z9783031249358
776 0 8 _iPrinted edition:
_z9783031249365
830 0 _aTexts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,
_x2197-8409
856 4 0 _uhttps://doi.org/10.1007/978-3-031-24934-1
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
942 _cSPRINGER
999 _c178542
_d178542