國立高雄大學圖資館 |

登入

回首頁

Concrete abstractionsformalizing and analyzing discrete theories and algorithms with the RISCAL model checker /

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Concrete abstractionsby Wolfgang Schreiner.
其他題名:	formalizing and analyzing discrete theories and algorithms with the RISCAL model checker /
作者:	Schreiner, Wolfgang.
出版者:	Cham :Springer International Publishing :2023.
面頁冊數:	xii, 271 p. :ill., digital ;24 cm.
Contained By:	Springer Nature eBook
標題:	Mathematical models.
電子資源:	https://doi.org/10.1007/978-3-031-24934-1
ISBN:	9783031249341$q(electronic bk.)

Concrete abstractionsformalizing and analyzing discrete theories and algorithms with the RISCAL model checker /
Schreiner, Wolfgang.

Concrete abstractionsformalizing and analyzing discrete theories and algorithms with the RISCAL model checker /[electronic resource] :by Wolfgang Schreiner. - Cham :Springer International Publishing :2023. - xii, 271 p. :ill., digital ;24 cm. - Texts & monographs in symbolic computation,2197-8409. - Texts & monographs in symbolic computation..

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.

ISBN: 9783031249341$q(electronic bk.)

Standard No.: 10.1007/978-3-031-24934-1doiSubjects--Topical Terms:

182479
Mathematical models.

LC Class. No.: TA342 / .S37 2023

Dewey Class. No.: 511.8

Concrete abstractionsformalizing and analyzing discrete theories and algorithms with the RISCAL model checker /
LDR:02317nmm a2200337 a 4500 001 642538
003 DE-He213
005 20230411153643.0
006 m d
007 cr nn 008maaau
008 231123s2023 sz s 0 eng d
020 $a 9783031249341$q(electronic bk.)
020 $a 9783031249334$q(paper)
024 7 $a 10.1007/978-3-031-24934-1 $2 doi
035 $a 978-3-031-24934-1
040 $a GP $c GP
041 0 $a eng
050 4 $a TA342 $b .S37 2023
072 7 $a UYAM $2 bicssc
072 7 $a COM018000 $2 bisacsh
072 7 $a UYAM $2 thema
082 0 4 $a 511.8 $2 23
090 $a TA342 $b .S378 2023
100 1 $a Schreiner, Wolfgang. $3 949887
245 1 0 $a Concrete abstractions $h [electronic resource] : $b formalizing and analyzing discrete theories and algorithms with the RISCAL model checker / $c by Wolfgang Schreiner.
260 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2023.
300 $a xii, 271 p. : $b ill., digital ; $c 24 cm.
490 1 $a Texts & monographs in symbolic computation, $x 2197-8409
505 0 $a 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.
520 $a 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.
650 0 $a Mathematical models. $3 182479
650 0 $a Mathematics $x Data processing. $3 185944
650 0 $a Algorithms. $3 184661
650 1 4 $a Mathematics of Computing. $3 273710
650 2 4 $a Computational Mathematics and Numerical Analysis. $3 274020
650 2 4 $a Mathematical Logic and Foundations. $3 274479
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer Nature eBook
830 0 $a Texts & monographs in symbolic computation. $3 726410
856 4 0 $u https://doi.org/10.1007/978-3-031-24934-1
950 $a Computer Science (SpringerNature-11645)