دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش:
نویسندگان: Wolfgang Schreiner
سری: Texts & Monographs in Symbolic Computation
ISBN (شابک) : 303124933X, 9783031249334
ناشر: Springer
سال نشر: 2023
تعداد صفحات: 277
[278]
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 4 Mb
در صورت تبدیل فایل کتاب Concrete Abstractions: Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب انتزاعات بتن: رسمیسازی و تحلیل نظریهها و الگوریتمهای گسسته با جستجوگر مدل RISCAL نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب نحوه مدلسازی رسمی حوزههای مختلف ریاضی (از جمله الگوریتمهای فعال در این حوزهها) را به گونهای نشان میدهد که آنها را قابل تجزیه و تحلیل کاملاً خودکار توسط نرمافزار رایانهای میکند. حوزههای ارائهشده معمولاً در ریاضیات گسسته، منطق، جبر و رایانه بررسی میشوند. علوم پایه؛ آنها در یک زبان رسمی مبتنی بر منطق مرتبه اول مدلسازی شدهاند که به اندازه کافی غنی است تا موجودیتهای اصلی را بیان کند که به درستی آنها علاقهمندیم: قضایای ریاضی و مشخصات الگوریتمی. این زبان رسمی زبان RISCAL است، یک \"بررسی مدل ریاضی\" که اعتبار همه فرمول ها و درستی همه الگوریتم ها را می توان به طور خودکار تعیین کرد. نرم افزار RISCAL به صورت رایگان در دسترس است. کلیه مطالب رسمی ارائه شده در کتاب در قالب فایل های مشخصات ارائه شده است که توسط آن خواننده می تواند در حین مطالعه مطالب کتاب مربوطه با نرم افزار تعامل داشته باشد.
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.
Preface Motivation Contents A Note on the Presentation Web Page and Software Acknowledgments Contents 1 Theories and Algorithms 1.1 Theories and Models 1.2 Theorems 1.3 Problems 1.4 Algorithms 1.5 Summary Further Reading 2 Searching and Sorting 2.1 Searching in Arrays 2.2 Loop Invariants and Termination Measures 2.3 Generating and Checking Verification Conditions 2.4 Constructing Invariants 2.5 Binary Search 2.6 Sorting Arrays 3 Sets, Relations, and Graphs 3.1 Sets 3.2 Relations and Directed Graphs 3.3 The Reachability of Nodes 3.4 Shortest Paths Between All Pairs of Nodes 3.5 Shortest Paths Between Two Nodes Further Reading 4 Propositional Logic 4.1 Boolean Algebras 4.2 Propositional Formulas 4.3 Clausal Normal Forms 4.4 Translating Propositional Formulas to Normal Forms 4.5 The Minimization of Disjunctive Normal Forms 4.6 The Satisfiability of Conjunctive Normal Forms Further Reading 5 Big Number and Polynomial Arithmetic 5.1 Arbitrary Precision Numbers 5.2 The Karatsuba Algorithm 5.3 Modular Arithmetic 5.4 Univariate Polynomials 5.5 Multivariate Polynomials Further Reading 6 Puzzles and Games 6.1 Chess Puzzles 6.2 Mathematical Puzzles 6.3 River-Crossing Puzzles 6.4 Games for Two Players Further Reading 7 Concurrent Systems 7.1 Peterson's Algorithm 7.2 The Alternating Bit Protocol 7.3 A Resource Allocator Further Reading 8 Further Topics 8.1 Checking Temporal Logic Specifications 8.2 Proving First-Order Formulas Further Reading A The RISCAL Software B RISCAL Models B.1 Theories and Algorithms B.2 Searching and Sorting B.3 Sets, Relations, and Graphs B.4 Propositional Logic B.5 Big Number and Polynomial Arithmetic B.6 Puzzles and Games B.7 Concurrent Systems References