03608nam 22006015 450 991068647560332120230518191723.09783031249341(electronic bk.)978303124933410.1007/978-3-031-24934-1(MiAaPQ)EBC7236307(Au-PeEL)EBL7236307(OCoLC)1376196151(DE-He213)978-3-031-24934-1(PPN)269656383(CKB)26428337000041(EXLCZ)992642833700004120230411d2023 u| 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierConcrete Abstractions Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker /by Wolfgang Schreiner1st ed. 2023.Cham :Springer International Publishing :Imprint: Springer,2023.1 online resource (278 pages)Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,2197-8409Print version: Schreiner, Wolfgang Concrete Abstractions Cham : Springer International Publishing AG,c2023 9783031249334 Includes bibliographical references.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.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.Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,2197-8409Computer science—MathematicsMathematics—Data processingLogic, Symbolic and mathematicalMathematics of ComputingComputational Mathematics and Numerical AnalysisMathematical Logic and FoundationsComputer science—Mathematics.Mathematics—Data processing.Logic, Symbolic and mathematical.Mathematics of Computing.Computational Mathematics and Numerical Analysis.Mathematical Logic and Foundations.511.8Schreiner Wolfgang1967-1236216MiAaPQMiAaPQMiAaPQ9910686475603321Concrete Abstractions3390443UNINA