مشخصات کتاب

Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings

دسته بندی: کنفرانس ها و همایش های بین المللی
ویرایش:  
نویسندگان: Konrad Slind,  Annette Bunker,  Ganesh C. Gopalakrishnan  
سری: Lecture notes in computer science 3223 
ISBN (شابک) : 3540230173, 9783540301424 
ناشر: Springer 
سال نشر: 2004 
تعداد صفحات: 349 
زبان: English 
فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 3 مگابایت 

در صورت تبدیل فایل کتاب Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب قضیه اثبات در منطق مرتبه بالاتر: هفدهمین کنفرانس بین المللی ، TPHOLS 2004 ، پارک سیتی ، یوتا ، ایالات متحده ، 14-17 سپتامبر 2004 ، مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.

توضیحاتی در مورد کتاب قضیه اثبات در منطق مرتبه بالاتر: هفدهمین کنفرانس بین المللی ، TPHOLS 2004 ، پارک سیتی ، یوتا ، ایالات متحده ، 14-17 سپتامبر 2004 ، مجموعه مقالات



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

21 مقاله کامل اصلاح شده ارائه شده است. به همراه 2 مقاله دعوت شده به دقت بررسی و از بین 42 مقاله ارسالی انتخاب شدند. از جمله موضوعات مطرح شده عبارتند از: اثبات قضیه، تأیید، انواع استقرایی، استنتاج خودکار، اثبات مکانیزه، منطق ریاضی، نظریه اثبات، سیستم‌های نوع، محاسبه‌پذیری، تأیید برنامه، ACL، Cop، Isabelle/HOL، توابع بازگشتی، نظریه ادغام، ایمنی کد ماشین. صدور گواهینامه و انتزاع

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

THis book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA in September 2004.

The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction.

فهرست مطالب

Front Matter....Pages -
Error Analysis of Digital Filters Using Theorem Proving....Pages 1-17
Verifying Uniqueness in a Logical Framework....Pages 18-33
A Program Logic for Resource Verification....Pages 34-49
Proof Reuse with Extended Inductive Types....Pages 50-65
Hierarchical Reflection....Pages 66-81
Correct Embedded Computing Futures....Pages 82-82
Higher Order Rippling in IsaPlanner ....Pages 83-98
A Mechanical Proof of the Cook-Levin Theorem....Pages 99-116
Formalizing the Proof of the Kepler Conjecture....Pages 117-117
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code....Pages 118-135
Extensible Hierarchical Tactic Construction in a Logical Framework....Pages 136-151
Theorem Reuse by Proof Term Transformation....Pages 152-167
Proving Compatibility Using Refinement....Pages 168-183
Java Program Verification via a JVM Deep Embedding in ACL2....Pages 184-200
Reasoning About CBV Functional Programs in Isabelle/HOL....Pages 201-216
Proof Pearl: From Concrete to Functional Unparsing....Pages 217-224
A Decision Procedure for Geometry in Coq....Pages 225-240
Recursive Function Definition for Types with Binders....Pages 241-256
Abstractions for Fault-Tolerant Distributed System Verification....Pages 257-270
Formalizing Integration Theory with an Application to Probabilistic Algorithms....Pages 271-286
Formalizing Java Dynamic Loading in HOL....Pages 287-304
Certifying Machine Code Safety: Shallow Versus Deep Embedding....Pages 305-320
Term Algebras with Length Function and Bounded Quantifier Alternation....Pages 321-336
Back Matter....Pages -

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

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

دانلود کتاب Wheat gluten: [the proceedings of the 7th International Workshop Gluten 2000 held at the University of Bristol on 2-6 April 2000]

دانلود کتاب Networks for Grid Applications: Second International Conference, GridNets 2008, Beijing, China, October 8-10, 2008, Revised Selected Papers

دانلود کتاب Automated Deduction in Geometry: Second International Workshop, ADG’98 Beijing, China, August 1–3, 1998 Proceedings

دانلود کتاب Society for General Microbiology. Symposium 60th. New challenges to health: the threat of virus infection

دانلود کتاب Approximation methods for Navier-Stokes problems. Proceedings symposium IUTAM, 1979

دانلود کتاب Proceedings symposium on value distribution theory in several complex variables

دانلود کتاب Commutative Algebra: Proceedings of a Workshop held in Salvador, Brazil, Aug. 8–17, 1988

دانلود کتاب Advanced Distributed Systems: Third International School and Symposium, ISSADS 2004, Guadalajara, Mexico, January 24-30, 2004, Revised Papers

دانلود کتاب Windpower Workshop

دانلود کتاب Computer and Computing Technologies in Agriculture II: The Second IFIP International Conference on Computer and Computing Technologies in Agriculture ... in Information and Communication Technology)