Concrete Abstractions : Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker / / by Wolfgang Schreiner
(Visualizza in formato marc)
(Visualizza in BIBFRAME)
| Autore: |
Schreiner Wolfgang <1967->
|
| Titolo: |
Concrete Abstractions : Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker / / by Wolfgang Schreiner
|
| Pubblicazione: | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 |
| Edizione: | 1st ed. 2023. |
| Descrizione fisica: | 1 online resource (278 pages) |
| Disciplina: | 511.8 |
| Soggetto topico: | Computer science - Mathematics |
| Mathematics - Data processing | |
| Logic, Symbolic and mathematical | |
| Mathematics of Computing | |
| Computational Mathematics and Numerical Analysis | |
| Mathematical Logic and Foundations | |
| Nota di bibliografia: | Includes bibliographical references. |
| Nota di contenuto: | 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. |
| Sommario/riassunto: | 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. |
| Titolo autorizzato: | Concrete Abstractions |
| ISBN: | 9783031249341 |
| 9783031249334 | |
| Formato: | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 9910686475603321 |
| Lo trovi qui: | Univ. Federico II |
| Opac: | Controlla la disponibilità qui |
Serie:
Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria, . 2197-8409