ورود به حساب

نام کاربری گذرواژه

گذرواژه را فراموش کردید؟ کلیک کنید

حساب کاربری ندارید؟ ساخت حساب

ساخت حساب کاربری

نام نام کاربری ایمیل شماره موبایل گذرواژه

برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید


09117307688
09117179751

در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید

دسترسی نامحدود

برای کاربرانی که ثبت نام کرده اند

ضمانت بازگشت وجه

درصورت عدم همخوانی توضیحات با کتاب

پشتیبانی

از ساعت 7 صبح تا 10 شب

دانلود کتاب The Clausal Theory of Types

دانلود کتاب نظریه ی قواعد انواع

The Clausal Theory of Types

مشخصات کتاب

The Clausal Theory of Types

دسته بندی: منطق
ویرایش:  
نویسندگان:   
سری: Cambridge Tracts in Theoretical Computer Science 21 
ISBN (شابک) : 0521117909, 9780521117906 
ناشر: CUP 
سال نشر: 1993 
تعداد صفحات: 133 
زبان: English 
فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 890 کیلوبایت

قیمت کتاب (تومان) : 41,000



ثبت امتیاز به این کتاب

میانگین امتیاز به این کتاب :
       تعداد امتیاز دهندگان : 15


در صورت تبدیل فایل کتاب The Clausal Theory of Types به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب نظریه ی قواعد انواع نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.


توضیحاتی در مورد کتاب نظریه ی قواعد انواع

این کتاب پایه های نظری یک زبان برنامه نویسی منطقی مرتبه بالاتر را با برابری، بر اساس نظریه بند انواع ارائه می کند. یک هدف طولانی برنامه‌نویسی منطقی، نظریه بند انواع، یک زبان برنامه‌نویسی منطقی است که امکان محاسبات تابعی را به عنوان یک عملیات ابتدایی فراهم می‌کند و در عین حال دارای معناشناسی دقیق، صریح و کامل اعلامی و عملیاتی است. این زبان بسیار قدرتمند است و از کسر معادله درجه بالاتر و محاسبات تابعی پشتیبانی می کند. نحو مرتبه بالاتر آن را مختصر و رسا می کند، انواع داده های انتزاعی را می توان در آن بیان کرد و جستجو برای راه حل های متعدد یک عملیات اساسی است. نویسنده تعدادی از نتایج مهم و شگفت‌انگیز را اثبات می‌کند: یک قضیه Skolem-Herbrand-G?del برای منطق مرتبه بالاتر. یک قضیه وضوح مرتبه بالاتر، که به عنوان موارد خاص شامل برخی حدس های اثبات نشده قبلی در مورد تطابق معادله و تطبیق مرتبه بالاتر است.


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

This book presents the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types. A long-sought goal of logic programming, the clausal theory of types is a logic programming language that allows functional computation as a primitive operation while having rigorous, sound, and complete declarative and operational semantics. The language is very powerful, supporting higher-order equational deduction and functional computation. Its higher order syntax makes it concise and expressive, abstract data types can be expressed in it, and searching for multiple solutions is a basic operation. The author proves a number of important and surprising results: a Skolem-Herbrand-G?del theorem for higher-order logic; a Higher-Order Resolution Theorem, which includes as special cases some previously unproven conjectures about equational matching and higher-order matching.



فهرست مطالب

Cover......Page 1
Cambridge Tracts in Theoretical Computer Science......Page 3
The Clausal Theory of Types......Page 4
9780521117906......Page 5
Contents......Page 6
Preface......Page 8
1.1.1 The Skolem-Herbrand-Godel Theorem......Page 10
1.1.3 Compound Instances......Page 12
1.1.4 Testing Validity......Page 13
1.1.5 Unsatisfiability Procedures......Page 14
1.2 Logic Programming......Page 16
1.2.2 Refutations and Answers......Page 18
1.2.4 Negation......Page 19
1.3 Discussion......Page 22
1.4 Overview of the Book......Page 23
2.1 Type Symbols......Page 26
2.2 Terms......Page 27
2.3.1 α-Conversion......Page 29
2.3.2 β-Reduction......Page 30
2.4 Normal Forms......Page 31
2.5 Substitutions......Page 33
3.1 Automating Higher-Order Logic......Page 36
3.2.1 Syntax......Page 38
3.3 General Models......Page 39
3.4 The Clausal Theory of Types......Page 41
3.4.2 Normal Form CTT Terms......Page 42
3.5 Term Structures......Page 45
3.5.1 λ-Models......Page 47
3.5.2 Properties of λ-Models......Page 49
3.6 The Higher-Order Theorem......Page 50
4.1 Higher-Order Equational Unification......Page 54
4.1.1 Higher-Order Term Rewriting Systems......Page 56
4.1.2 Soundness and Completeness......Page 60
4.1.3 Third-Order Equational Matching......Page 63
4.2 Higher-Order Unification......Page 64
4.2.1 Higher-Order Unifiers......Page 65
4.2.2 Higher-Order Pre-Unification Procedure......Page 66
4.2.3 Heuristics and Implementations......Page 68
4.2.4 Undecidability Results......Page 70
4.3.1 Freezing Lemma......Page 73
4.4.1 Examples of Nontermination......Page 74
4.4.2 Removing Constant Symbols......Page 75
4.4.3 An Algorithm for Higher-Order Matching......Page 77
4.4.4 Plotkin-Statman Conjecture......Page 82
4.4.5 Decidable Matching Problems......Page 85
4.4.6 Regular Unification Problems......Page 89
4.5 Second-Order Monadic Unification......Page 93
4.5.1 Decidability and the Monoid Problem......Page 95
4.6 First-Order Equational Unification......Page 96
5.1 Higher-Order Equational Resolution......Page 98
5.1.1 ~-λ-Models and Closed Resolution......Page 100
5.1.2 The General Level......Page 101
5.2 CTT and Logic Programming......Page 103
5.2.1 Least CTT Models......Page 105
5.2.2 Least Fixed Points......Page 107
5.2.3 BF- and SLD-resolution......Page 109
5.2.4 Soundness and Completeness......Page 111
5.2.5 Declarative and Operational Semantics......Page 113
5.3 Discussion......Page 114
Bibliography......Page 116
Index......Page 130




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

تمامی حقوق معنوی و مادی وبسایت متعلق به اینترنشنال لایبرری می باشد
نماد اعتماد الکترونیکی