دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: منطق ویرایش: 1 نویسندگان: Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, Wolfgang Paul (auth.), Joe Hurd, Tom Melham (eds.) سری: Lecture Notes in Computer Science 3603 : Theoretical Computer Science and General Issues ISBN (شابک) : 3540283722, 9783540283720 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2005 تعداد صفحات: 417 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 3 مگابایت
در صورت ایرانی بودن نویسنده امکان دانلود وجود ندارد و مبلغ عودت داده خواهد شد
کلمات کلیدی مربوط به کتاب قضیه اثبات در منطق مرتبه بالاتر: هجدهمین کنفرانس بین المللی ، TPHOLs 2005 ، آکسفورد ، انگلستان ، 22-25 اوت 2005. مجموعه مقالات: منطق ریاضی و زبان های رسمی، منطق و معانی برنامه ها، مهندسی نرم افزار، هوش مصنوعی (شامل رباتیک)، طراحی منطقی
در صورت تبدیل فایل کتاب Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب قضیه اثبات در منطق مرتبه بالاتر: هجدهمین کنفرانس بین المللی ، TPHOLs 2005 ، آکسفورد ، انگلستان ، 22-25 اوت 2005. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این جلد مجموعه مقالات هجدهمین کنفرانس بینالمللی اثبات قضیه در منطقهای مرتبه بالاتر (TPHOLs 2005) است که طی 22 تا 25 آگوست 2005 در آکسفورد، انگلستان برگزار شد. ?کاتیون. 49 مقاله در گروه تحقیقاتی کامل به TPHOLs 2005 ارسال شد که هر یک توسط حداقل سه داور انتخاب شده توسط کمیته برنامه داوری شده بودند. از این تعداد 20 مقاله پژوهشی و 4 مروارید اثبات برای ارائه در کنفرانس و انتشار در این جلد پذیرفته شد. مطابق با سنت دیرینه، TPHOLs 2005 همچنین مکانی را برای ارائه کارهای در دست اجرا ایجاد کرد، جایی که محققان از طریق یک سخنرانی مقدماتی مختصر به بحث و گفتگو دعوت کردند و سپس کار خود را در یک جلسه پوستر مورد بحث قرار دادند. یک دوره تکمیلی به عنوان یک گزارش فنی در سال 2005 از آزمایشگاه محاسبات دانشگاه آکسفورد منتشر شد. سازمان دهندگان از ولفگانگ پل و اندرو پیتس به خاطر موافقت با برگزاری سخنرانی های دعوت شده در TPHOLs 2005 سپاسگزار هستند.
This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22–25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.
Front Matter....Pages -
On the Correctness of Operating System Kernels....Pages 1-16
Alpha-Structural Recursion and Induction....Pages 17-34
Shallow Lazy Proofs....Pages 35-49
Mechanized Metatheory for the Masses: The P opl M ark Challenge....Pages 50-65
A Structured Set of Higher-Order Problems....Pages 66-81
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS....Pages 82-97
Proving Equalities in a Commutative Ring Done Right in Coq....Pages 98-113
A HOL Theory of Euclidean Space....Pages 114-129
A Design Structure for Higher Order Quotients....Pages 130-146
Axiomatic Constructor Classes in Isabelle/HOLCF....Pages 147-162
Meta Reasoning in ACL2....Pages 163-178
Reasoning About Java Programs with Aliasing and Frame Conditions....Pages 179-194
Real Number Calculations and Theorem Proving....Pages 195-210
Verifying a Secure Information Flow Analyzer....Pages 211-226
Proving Bounds for Real Linear Programs in Isabelle/HOL....Pages 227-244
Essential Incompleteness of Arithmetic Verified by Coq....Pages 245-260
Verification of BDD Normalization....Pages 261-277
Extensionality in the Calculus of Constructions....Pages 278-293
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic....Pages 294-309
A Generic Network on Chip Model....Pages 310-325
Formal Verification of a SHA-1 Circuit Core Using ACL2....Pages 326-341
From PSL to LTL: A Formal Validation in HOL....Pages 342-357
Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2....Pages 358-372
Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2....Pages 373-384
Proof Pearl: Defining Functions over Finite Sets....Pages 385-396
Proof Pearl: Using Combinators to Manipulate let -Expressions in Proof....Pages 397-408
Back Matter....Pages -