دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
دانلود کتاب قضیه تعاملی ارائه: چهارمین کنفرانس بین المللی ، ITP 2013 ، رن ، فرانسه ، 22-26 ژوئیه ، 2013. مجموعه مقالات
مشخصات کتاب
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
ویرایش: 1 نویسندگان: Dominique Bolignano (auth.), Sandrine Blazy, Christine Paulin-Mohring, David Pichardie (eds.) سری: Lecture Notes in Computer Science 7998 ISBN (شابک) : 9783642396335, 9783642396342 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2013 تعداد صفحات: 508 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 5 مگابایت
قیمت کتاب (تومان) : 60,000
کلمات کلیدی مربوط به کتاب قضیه تعاملی ارائه: چهارمین کنفرانس بین المللی ، ITP 2013 ، رن ، فرانسه ، 22-26 ژوئیه ، 2013. مجموعه مقالات: منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)، منطق و معانی برنامه ها، مهندسی نرم افزار، سیستم ها و امنیت داده ها، تجزیه و تحلیل الگوریتم و پیچیدگی مسائل
در صورت تبدیل فایل کتاب Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب قضیه تعاملی ارائه: چهارمین کنفرانس بین المللی ، ITP 2013 ، رن ، فرانسه ، 22-26 ژوئیه ، 2013. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب قضیه تعاملی ارائه: چهارمین کنفرانس بین المللی ، ITP 2013 ، رن ، فرانسه ، 22-26 ژوئیه ، 2013. مجموعه مقالات
این کتاب مجموعه مقالات داوری چهارمین کنفرانس بین‌المللی اثبات قضیه تعاملی، ITP 2013، که در رن، فرانسه، در ژوئیه 2013 برگزار شد، تشکیل شده است. 2 آموزش دعوت شده با دقت بررسی و از بین 66 مورد ارسالی انتخاب شدند. مقالات در بخش‌های موضوعی مانند تأیید برنامه، امنیت، رسمی‌سازی ریاضیات و توسعه اثبات قضیه سازمان‌دهی شده‌اند.
توضیحاتی درمورد کتاب به خارجی
This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.
فهرست مطالب
Front Matter....Pages -
Applying Formal Methods in the Large....Pages 1-1
Automating Theorem Proving with SMT....Pages 2-16
Certifying Voting Protocols....Pages 17-17
Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities....Pages 18-18
Canonical Structures for the Working Coq User....Pages 19-34
MaSh: Machine Learning for Sledgehammer....Pages 35-50
Scalable LCF-Style Proof Translation....Pages 51-66
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation....Pages 67-83
Automatic Data Refinement....Pages 84-99
Data Refinement in Isabelle/HOL....Pages 100-115
Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable....Pages 116-132
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1 ....Pages 133-146
Mechanising Turing Machines and Computability Theory in Isabelle/HOL....Pages 147-162
A Machine-Checked Proof of the Odd Order Theorem....Pages 163-179
Kleene Algebra with Tests and Coq Tools for while Programs....Pages 180-196
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL....Pages 197-212
Pragmatic Quotient Types in Coq ....Pages 213-228
Mechanical Verification of SAT Refutations with Extended Resolution....Pages 229-244
Formalizing Bounded Increase....Pages 245-260
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types....Pages 261-278
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL....Pages 279-294
Formal Reasoning about Classified Markov Chains in HOL....Pages 295-310
Practical Probability: Applying pGCL to Lattice Scheduling....Pages 311-327
Adjustable References....Pages 328-337
Handcrafted Inversions Made Operational on Operational Semantics....Pages 338-353
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques....Pages 354-369
Program Extraction from Nested Definitions....Pages 370-385
Subformula Linking as an Interaction Method....Pages 386-401
Automatically Generated Infrastructure for De Bruijn Syntaxes....Pages 402-417
Shared-Memory Multiprocessing for Interactive Theorem Proving....Pages 418-434
A Parallelized Theorem Prover for a Logic with Parallel Execution....Pages 435-450
Communicating Formal Proofs: The Case of Flyspeck....Pages 451-456
Square Root and Division Elimination in PVS....Pages 457-462
The Picard Algorithm for Ordinary Differential Equations in Coq....Pages 463-468
Stateless Higher-Order Logic with Quantified Types....Pages 469-476
Implementing Hash-Consed Structures in Coq....Pages 477-483
Towards Certifying Network Calculus....Pages 484-489
Steps towards Verified Implementations of HOL Light....Pages 490-495
Back Matter....Pages -
نظرات کاربران
کتاب های تصادفی
دانلود کتاب Dakota Grammar: With Texts and Ethnography
دانلود کتاب Methylphenidate - A Medical Dictionary, Bibliography, and Annotated Research Guide to Internet References
دانلود کتاب Stones of the New Consciousness: Healing, Awakening, and Co-creating with Crystals, Minerals, and Gems
دانلود کتاب America: Standing Strong
