|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910686475603321 |
|
|
Autore |
Schreiner Wolfgang <1967-> |
|
|
Titolo |
Concrete Abstractions : Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker / / by Wolfgang Schreiner |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 |
|
|
|
|
|
|
|
|
|
ISBN |
|
9783031249341 |
9783031249334 |
|
|
|
|
|
|
|
|
Edizione |
[1st ed. 2023.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (278 pages) |
|
|
|
|
|
|
Collana |
|
Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria, , 2197-8409 |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computer science—Mathematics |
Mathematics—Data processing |
Logic, Symbolic and mathematical |
Mathematics of Computing |
Computational Mathematics and Numerical Analysis |
Mathematical Logic and Foundations |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
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 |
|
|
|
|