مشخصات کتاب

Theorem Proving in Higher Order Logics: 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings

دسته بندی: منطق
ویرایش: 1 
نویسندگان: Constance L. Heitmeyer (auth.),  Klaus Schneider,  Jens Brandt (eds.)  
سری: Lecture Notes in Computer Science 4732 
ISBN (شابک) : 3540745904, 9783540745907 
ناشر: Springer-Verlag Berlin Heidelberg 
سال نشر: 2007 
تعداد صفحات: 407 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 3 مگابایت 

کلمات کلیدی مربوط به کتاب قضیه تئوری منطق سفارش بالاتر: 20مین کنفرانس بین المللی، TPHOLs 2007، Kaiserslautern، Germany، 10-13 سپتامبر 2007. پرونده ها: منطق ریاضی و زبان های رسمی، منطق و معانی برنامه ها، مهندسی نرم افزار، هوش مصنوعی (شامل رباتیک)، طراحی منطقی

در صورت تبدیل فایل کتاب Theorem Proving in Higher Order Logics: 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب قضیه تئوری منطق سفارش بالاتر: 20مین کنفرانس بین المللی، TPHOLs 2007، Kaiserslautern، Germany، 10-13 سپتامبر 2007. پرونده ها نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.

توضیحاتی در مورد کتاب قضیه تئوری منطق سفارش بالاتر: 20مین کنفرانس بین المللی، TPHOLs 2007، Kaiserslautern، Germany، 10-13 سپتامبر 2007. پرونده ها



این کتاب مجموعه مقالات داوری بیستمین کنفرانس بین‌المللی اثبات قضیه در منطق‌های مرتبه بالاتر، TPHOLs 2007 است که در کایزرسلاوترن، آلمان، در سپتامبر 2007 برگزار شد.

21 مقاله کامل اصلاح‌شده همراه با ارائه شده است. 5 مروارید اثبات (ارائه مختصر و ظریف نمونه های جالب) و چکیده 3 مقاله دعوت شده با دقت بررسی و از بین 52 مورد ارسالی انتخاب شدند. از جمله موضوعات این جلد می‌توان به معناشناسی رسمی مشخصات، مدل‌سازی و زبان‌های برنامه‌نویسی، مشخصات و تأیید سخت‌افزار و نرم‌افزار، رسمی‌سازی نظریه‌های ریاضی، پیشرفت در فناوری اثبات قضیه و همچنین کاربرد صنعتی اثبات‌کننده‌های قضیه اشاره کرد.

توضیحاتی درمورد کتاب به خارجی

This book constitutes the refereed proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, held in Kaiserslautern, Germany, in September 2007.

The 21 revised full papers presented together with 5 proof pearls (concise and elegant presentations of interesting examples) and the abstracts of 3 invited papers were carefully reviewed and selected from 52 submissions. Among the topics of this volume are formal semantics of specification, modelling, and programming languages, specification and verification of hardware and software, formalisation of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.

فهرست مطالب

Front Matter....Pages -
On the Utility of Formal Methods in the Development and Certification of Software....Pages 1-2
Formal Techniques in Software Engineering: Correct Software and Safe Systems....Pages 3-4
Separation Logic for Small-Step cminor ....Pages 5-21
Formalising Java’s Data Race Free Guarantee....Pages 22-37
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL....Pages 38-53
Formalising Generalised Substitutions....Pages 54-69
Extracting Purely Functional Contents from Logical Inductive Types....Pages 70-85
A Modular Formalisation of Finite Group Theory....Pages 86-101
Verifying Nonlinear Real Formulas Via Sums of Squares....Pages 102-118
Verification of Expectation Properties for Discrete Random Variables in HOL....Pages 119-134
A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic....Pages 135-150
Proof Pearl: The Termination Analysis of Terminator ....Pages 151-156
Improving the Usability of HOL Through Controlled Automation Tactics....Pages 157-172
Verified Decision Procedures on Context-Free Grammars....Pages 173-188
Using XCAP to Certify Realistic Systems Code: Machine Context Management....Pages 189-206
Proof Pearl: De Bruijn Terms Really Do Work....Pages 207-222
Proof Pearl: Looping Around the Orbit....Pages 223-231
Source-Level Proof Reconstruction for Interactive Theorem Proving....Pages 232-245
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF....Pages 246-261
Automatically Translating Type and Function Definitions from HOL to ACL2....Pages 262-277
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models....Pages 278-293
Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0 ....Pages 294-301
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols....Pages 302-318
Primality Proving with Elliptic Curves....Pages 319-333
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism....Pages 334-351
Building Formal Method Tools in the Isabelle/Isar Framework....Pages 352-367
Simple Types in Type Theory: Deep and Shallow Encodings....Pages 368-382
Mizar’s Soft Type System....Pages 383-399
Back Matter....Pages -

نظرات کاربران

کتاب های مرتبط

دانلود کتاب Formal Aspects of Context

دانلود کتاب Geometric Stability Theory

دانلود کتاب Algebraic semantics

دانلود کتاب Mathematical Logic

دانلود کتاب Isabelle/HOL: A Proof Assistant for Higher-Order Logic

دانلود کتاب A Guide to Classical and Modern Model Theory

دانلود کتاب Orthogonality and Quantum Geometry: Towards a Relational Reconstruction of Quantum Theory [PhD Thesis]

دانلود کتاب An Introduction to Substructural Logics

دانلود کتاب The Ideological Origins of Nazi Imperialism

دانلود کتاب Origins of Logical Empiricism