検索結果をRefWorksへエクスポートします。対象は1件です。
Export
RT Book, Whole SR Electronic DC OPAC T1 Concrete Abstractions : Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker / by Wolfgang Schreiner T2 Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria. ISSN:21978409 A1 Schreiner, Wolfgang A1 SpringerLink (Online service) YR 2023 FD 2023 SP XII, 271 p. 79 illus., 53 illus. in color K1 Computer science -- Mathematics K1 Mathematics -- Data processing K1 Mathematical logic K1 Mathematics of Computing K1 Computational Mathematics and Numerical Analysis K1 Mathematical Logic and Foundations ED 1st ed. 2023. PB Springer International Publishing : Imprint: Springer PP Cham SN 9783031249341 LA English (英語) CL LCC:QA76.9.M35 CL DC23:004.0151 NO 1. 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 NO This 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 NO HTTP:URL=https://doi.org/10.1007/978-3-031-24934-1 NO 書誌ID=EB00002002; LK [E Book]https://doi.org/10.1007/978-3-031-24934-1 OL 30