مشخصات کتاب

Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics [PhD Thesis]

دسته بندی: منطق
ویرایش:  
نویسندگان: Lincoln A. Wallen  
سری:  
ISBN (شابک) : 0262231441 
ناشر: The MIT Press 
سال نشر: 1990 
تعداد صفحات: 252 
زبان: English 
فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 2 مگابایت 

در صورت تبدیل فایل کتاب Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics [PhD Thesis] به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب جستجوی خودکار اثبات در منطق های غیر کلاسیک: روش های اثبات ماتریسی کارآمد برای منطق های معین و شهودی [پایان نامه دکتری] نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.

توضیحاتی در مورد کتاب جستجوی خودکار اثبات در منطق های غیر کلاسیک: روش های اثبات ماتریسی کارآمد برای منطق های معین و شهودی [پایان نامه دکتری]

این کتاب نسخه اصلاح شده دکترای من است. پایان نامه ارسال شده به بخش هوش مصنوعی دانشگاه ادینبورگ اسکاتلند زیر نظر پروفسور آلن باندی. اگرچه رویای قرن هفدهمی لایب نیتس در مورد زبانی نمادین برای بازنمایی و حل مکانیکی همه مسائل علمی و ریاضی به دلیل عدم تصمیم گیری، ناقص بودن و استقلال نتایج منطق ریاضی مدرن آسیب دیده است، روح ایده او در محاسبات زنده است. علوم پایه. حل مکانیکی مسائل با آزمایش جملات یک منطق نمادین برای قضیه با استفاده از رایانه عملی شده است، حتی اگر مشکل تصمیم گیری برای منطق ممکن است از نظر فنی غیرقابل حل باشد. عملکرد عملی الگوریتم‌ها برای چنین کسر خودکار - یا جستجوی اثبات خودکار - را می‌توان با تکنیک‌های بهینه‌سازی استاندارد، ساختارهای داده جدید و سخت‌افزار قدرتمندتر بهبود بخشید، اما در تحلیل نهایی الگوریتم‌های موفق از ویژگی‌های محاسباتی حساس خود منطق‌ها ناشی می‌شوند. در این کتاب تعدادی از این خصوصیات محاسباتی حساس برای منطق های مرتبه اول مختلف توسعه داده شده است. هدف این بوده است که با ارائه شواهد تجربی مبنی بر وجود رویکردی یکسان برای جستجوی اثبات کارآمد در هر دو منطق کارکردی حقیقت و غیرحقیقت، زمینه‌ای برای نظریه استنتاج خودکار در منطق‌های نمادین دلخواه فراهم شود.

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

This book is a revised version of my PhD. dissertation submitted to the Dept. of Artificial Intelligence, University of Edinburgh, Scotland, under the supervision of Prof. Alan Bundy. Although Leibniz' seventeenth-century dream of a symbolic language for the representation and mechanical solution of all scientific and mathematical problems has suffered at the hands of the undecidability, incompleteness and independence results of modern mathematical logic, the spirit of his idea lives on within Computing Science. It has proved practical to solve problems mechanically by testing sentences of a symbolic logic for theoremhood using a computer, even though the decision problem for the logic might be technically intractable. The practical performance of algorithms for such automated deduction — or automated proof search — can be improved by standard optimisation techniques, novel data structures and more powerful hardware, but in the final analysis successful algorithms arise from computationally sensitive characterisations of the logics themselves. In this book a number of such computationally sensitive characterisations are developed for various first-order logics. The aim has been to lay the groundwork for a theory of automated deduction in arbitrary symbolic logics by providing empirical evidence for the existence of a uniform approach to efficient proof search in both truth-functional and non truth-functional logics.

فهرست مطالب

Contents ......Page 4
List of figures ......Page 6
List of tables ......Page 8
Series foreword ......Page 9
Acknowledgements ......Page 10
Introduction ......Page 11
PART I. CLASSICAL LOGIC ......Page 15
Introduction to Part I ......Page 17
§1. Syntax and semantics ......Page 19
§2. The sequent calculus ......Page 22
§3. Search methods ......Page 26
§4. Redundancy in the sequent search space ......Page 31
§1. Introduction ......Page 39
§2. Formula trees and notational redundancy ......Page 42
§3. Paths, connections and irrelevance ......Page 54
§4. Reduction orderings and permutability ......Page 60
PART II. MODAL LOGIC ......Page 67
Introduction to Part II ......Page 69
§1. Syntax, semantics and notation ......Page 71
§2. Sequent calculi for modal logics ......Page 77
§3. S5 and constant domain modal logics ......Page 89
§1. Introduction ......Page 92
§2. Notational redundancy and relevance ......Page 93
§3. Non-permutability ......Page 95
§4. Interactions: modal operators and quantifiers ......Page 97
§1. Introduction ......Page 101
§2. Matrices, paths and connections ......Page 106
§3. Correctness ......Page 129
§4. Completeness ......Page 155
§2. Unification problems ......Page 164
§3. Proof search in the matrix systems ......Page 170
§4. Decision procedures ......Page 186
§5. Logical consequence and expressibility ......Page 196
§1. Introduction ......Page 198
§2. Sequent and tableau-based proof systems ......Page 199
§3. Resolution-based proof systems ......Page 201
§4. Hybrid systems ......Page 207
PART III. INTUITIONISTIC LOGIC ......Page 211
Introduction to Part III ......Page 213
§4. Introduction ......Page 215
§2. Kripke semantics for J ......Page 216
§3. A cut-free sequent calculus for J ......Page 217
§4. A matrix characterisation of validity in J ......Page 220
§5. Correctness and completeness ......Page 231
§6. Alternative proof methods ......Page 233
§7. Summary ......Page 234
Conclusion ......Page 235
Bibliography ......Page 238
Index of symbols ......Page 245
Index ......Page 246

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

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

دانلود کتاب Many-Valued Logics for Modeling Vagueness

دانلود کتاب Technological Transitions And System Innovations: A Co-evolutionary And Socio-technical Analysis

دانلود کتاب Games and Infinitary Languages

دانلود کتاب Book of proof

دانلود کتاب Interactive Logic: Selected Papers from the 7th Augustus de Morgan Workshop, London

دانلود کتاب Church's Thesis After 70 Years

دانلود کتاب Normalization, Cut-Elimination, and the Theory of Proofs

دانلود کتاب An Algebraic Approach to Incompleteness in Modal Logic [PhD Thesis]

دانلود کتاب Epistemic Dynamics and Protocol Information [PhD Thesis]

دانلود کتاب Handbook of Logic in Artificial Intelligence and Logic Programming. Volume 4: Epistemic and Temporal Reasoning