دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Antonia Balaa, Yves Bertot (auth.), Mark Aagaard, John Harrison (eds.) سری: Lecture Notes in Computer Science 1869 ISBN (شابک) : 9783540678632, 3540678638 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2000 تعداد صفحات: 546 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 11 مگابایت
کلمات کلیدی مربوط به کتاب قضیه اثبات در منطق مرتبه بالاتر: سیزدهمین کنفرانس بین المللی ، TPHOLs 2000 پورتلند ، ایالت ، ایالات متحده ، 14-18-18 اوت مجموعه مقالات: منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)، منطق و معانی برنامه ها، مهندسی نرم افزار، طراحی منطق
در صورت تبدیل فایل کتاب Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14–18, 2000 Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب قضیه اثبات در منطق مرتبه بالاتر: سیزدهمین کنفرانس بین المللی ، TPHOLs 2000 پورتلند ، ایالت ، ایالات متحده ، 14-18-18 اوت مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این جلد مجموعه مقالات سیزدهمین کنفرانس بین المللی اثبات تئوریم در منطق های مرتبه عالی (TPHOLs 2000) است که از 14 تا 18 اوت 2000 در پورتلند، اورگان، ایالات متحده برگزار شد. هر یک از 55 مقاله ارسال شده در رده تحقیق کامل توسط حداقل سه داور که توسط کمیته برنامه انتخاب شده بودند داوری شدند. به دلیل فضای محدود موجود در برنامه و مجموعه مقالات، تنها 29 مقاله برای ارائه و چاپ در این جلد پذیرفته شد. مطابق با سنت، TPHOLs 2000 همچنین مکانی را برای ارائه کارهای در دست اجرا ارائه کرد، جایی که محققان با استفاده از یک سخنرانی مقدماتی مختصر به بحث دعوت میکنند و سپس در یک جلسه پوستر درباره کار خود بحث میکنند. یک دادرسی تکمیلی حاوی مقالات مرتبط برای کار در حال انجام توسط مؤسسه فارغ التحصیلان اورگان (OGI) به عنوان گزارش فنی CSE-00-009 منتشر شد. برگزارکنندگان از باب کولول، رابین میلنر و لری ووس به خاطر موافقت با انجام مذاکرات دعوت شده تشکر می کنند. باب کولول معمار اصلی ریزمعماری Intel P6 بود که تعدادی از تکنیک های نوآورانه را معرفی کرد و به موفقیت تجاری عظیمی دست یافت. به این ترتیب، او در موقعیت ایده آلی برای ارائه دیدگاه صنعتی در مورد چالش های تأیید رسمی قرار دارد. رابین میلنر از طریق رهبری پروژه تأثیرگذار ادینبورگ LCF، ایده های کلیدی بسیاری را برای اثبات قضیه رایانه و برنامه نویسی تابعی ارائه کرد.
This volume is the proceedings of the 13th International Conference on Theo rem Proving in Higher Order Logics (TPHOLs 2000) held 14-18 August 2000 in Portland, Oregon, USA. Each of the 55 papers submitted in the full rese arch category was refereed by at least three reviewers who were selected by the program committee. Because of the limited space available in the program and proceedings, only 29 papers were accepted for presentation and publication in this volume. In keeping with tradition, TPHOLs 2000 also offered a venue for the presen tation of work in progress, where researchers invite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplemen tary proceedings containing associated papers for work in progress was published by the Oregon Graduate Institute (OGI) as technical report CSE-00-009. The organizers are grateful to Bob Colwell, Robin Milner and Larry Wos for agreeing to give invited talks. Bob Colwell was the lead architect on the Intel P6 microarchitecture, which introduced a number of innovative techniques and achieved enormous commercial success. As such, he is ideally placed to offer an industrial perspective on the challenges for formal verification. Robin Milner contributed many key ideas to computer theorem proving, and to functional programming, through his leadership of the influential Edinburgh LCF project.
Fix-Point Equations for Well-Founded Recursion in Type Theory....Pages 1-16
Programming and Computing in HOL....Pages 17-37
Proof Terms for Simply Typed Higher Order Logic....Pages 38-52
Routing Information Protocol in HOL/SPIN....Pages 53-72
Recursive Families of Inductive Types....Pages 73-89
Aircraft Trajectory Modeling and Alerting Algorithm Verification....Pages 90-105
Intel’s Formal Verification Experience on the Willamette Development....Pages 106-107
A Prototype Proof Translator from HOL to Coq....Pages 108-125
Proving ML Type Soundness Within Coq....Pages 126-144
On the Mechanization of Real Analysis in Isabelle/HOL....Pages 145-161
Equational Reasoning via Partial Reflection....Pages 162-178
Reachability Programming in HOL98 Using BDDs....Pages 179-196
Transcendental Functions and Continuity Checking in PVS....Pages 197-214
Verified Optimizations for the Intel IA-64 Architecture....Pages 215-232
Formal Verification of IA-64 Division Algorithms....Pages 233-251
Fast Tactic-Based Theorem Proving....Pages 252-267
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover....Pages 268-282
A Strong and Mechanizable Grand Logic....Pages 283-300
Inheritance in Higher Order Logic: Modeling and Reasoning....Pages 301-319
Total-Correctness Refinement for Sequential Reactive Systems....Pages 320-337
Divider Circuit Verification with Model Checking and Theorem Proving....Pages 338-355
Specification and Verification of a Steam-Boiler with Signal-Coq....Pages 356-371
Functional Procedures in Higher-Order Logic....Pages 372-387
Formalizing Stålmarck’s Algorithm in Coq....Pages 388-405
TAS — A Generic Window Inference System....Pages 406-423
Weak Alternating Automata in Isabelle/HOL....Pages 424-441
Graphical Theories of Interactive Systems: Can a Proof Assistant Help?....Pages 442-442
Formal Verification of the Alpha 21364 Network Protocol....Pages 443-461
Dependently Typed Records for Representing Mathematical Structure....Pages 462-479
Towards a Machine-Checked Java Specification Book....Pages 480-497
Another Look at Nested Recursion....Pages 498-518
Automating the Search for Answers to Open Questions....Pages 519-525
Appendix: Conjectures Concerning Proof, Design, and Verification....Pages 526-533