Efficient Deduction in Many-Valued Logics

دسته بندی: منطق
ویرایش:  
نویسندگان: Hahnle R.  
سری:  
 
ناشر:  
سال نشر:  
تعداد صفحات: 10 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 277 کیلوبایت 

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

اینترنت-انتشارات. - 10 ص. انگلیسی. (OCR-слой). [Reiner Hahnle. دانشگاه کارلسروهه موسسه منطق، پیچیدگی و سیستم های قیاسی. کارلسروهه، آلمان]. چکیده.
این مقاله سعی دارد مشکلات اساسی را که در قضیه خودکار اثبات شده در بسیاری از برای منطق ها ارزش قائل است و نشان می دهد که در حال حاضر تا چه اندازه می توان آنها را حل کرد. برای این منظور تعدادی از تکنیک های اخیرا توسعه یافته بررسی می شوند. ما راه‌های تحقیق را در قضیه‌های چند ارزشی فهرست می‌کنیم که ثابت می‌کند از نظر ما امیدوارکننده‌ترین هستند. مقدمه.
هدف این یادداشت مرور تعدادی از تکنیک‌هایی است که منجر به نمایش محاسباتی کافی از فضای جستجوی منطق‌های چند ارزشی می‌شوند و شناسایی راه‌های تحقیق در قضیه‌های چند ارزشی است که در نظر ما امیدوارکننده‌ترین هستند. ما به تعداد زیاد کاربردهای احتمالی اثبات قضیه چند ارزشی اشاره نمی‌کنیم، اما برای فهرست گسترده‌ای از کاربردها به [15] و برای مطالعه موردی به [18] مراجعه کنید.
اگر کسی ارزش‌های زیادی را انجام می‌دهد. استنتاج، معمولاً تعدادی از مشکلات که در استنتاج کلاسیک چندان برجسته نیستند، باید مورد توجه قرار گیرند:
تعداد تمایز موارد به دلیل افزایش تعداد مقادیر صدق بسیار بیشتر است.
میزان افزونگی در کسر بسیار بزرگتر است. به طور معمول، اتصالات با ارزش‌های زیاد درجه خاصی از نظم را نشان می‌دهند و باید راه‌هایی برای بهره‌برداری از آن پیدا کرد.
به طور کلی، فرم‌های عادی داخلی (یعنی فرم‌های معمولی که صرفاً بر اساس پیوندهای منطق مورد بررسی است.) در دسترس نیستند.
در مورد منطق‌های با ارزش بی‌نهایت، مشکل یافتن یک نمایش محدود از فضای جستجو وجود دارد. مقدمه .
منطق چند ارزشی.
تعریف - (Syntax).
تعریف - (ارزشهای حقیقت، معنایی، منطق).
تعریف - (ارزش گذاری).
تعریف - (S-رضایت پذیری، -نتیجه).
تعریف - (Syntax مرتبه اول).
تعریف - (معناشناسی/منطق مرتبه اول).< br/> مثال - منطق لوکاسیویچ.
به‌عنوان نشانه‌ها تنظیم می‌شود.
تعریف - (فرمول امضا شده).
منطق‌های منظم.
تعریف - (دایره، گوشه) [13]).
تعریف - (منطق منظم [13]).
تعریف - (مجموعه مرتب شده جزئی).
تعریف - (بالا، پایین).
فرم‌های عادی.
رزولوشن، نسخه موازی: تعریف - (تفریح ​​امضا شده).
برنامه‌نویسی عدد صحیح.
پیاده‌سازی.
نتیجه گیری و چشم انداز.
مرجع (30 انتشارات).

Internet-Publication. — 10 p. English. (OCR-слой). [Reiner Hahnle. University of Karlsruhe. Institute for Logic, Complexity and Deduction Systems. Karlsruhe, Germany]. Abstract.
This paper tries to identify the basic problems encountered in automated theorem proving in many-valued logics and demonstrates to which extent they can be currently solved. To this end a number of recently developed techniques are reviewed. We list the avenues of research in many-valued theorem proving that are in our eyes the most promising. Introduction.
The purpose of this note is to review a number of techniques that lead to a computationally adequate representation of the search space of many-valued logics and to identify the avenues of research in many-valued theorem proving that are in our eyes the most promising. We do not mention the large number of possible applications of many-valued theorem proving, but refer to [15] for an extensive list of applications and to [18] for a case study.
If one is doing many-valued deduction, typically a number of problems that are not as much prominent in classical deduction have to be addressed:
The number of case distinctions is much larger due to the increased number of truth values.
The amount of redundancy in deductions is much bigger. Typically, many-valued connectives show a certain degree of regularity and one has to nd ways of how to exploit this.
In general, internal normal forms (that is, normal forms based solely on connectives from the logic under consideration) are not available.
In the case of infinitely-valued logics there is the problem to find a finite representation of the search space. Introduction.
Many-Valued Logic.
Definition - (Syntax).
Definition - (Truth Values, Semantic, Logic).
Definition - (Valuation).
Definition - (S-Satisfiability, -Consequence).
Definition - (First-Order Syntax).
Definition - (First-Order Semantics/Logic).
Example - Lukasiewicz Logics.
Sets as Signs.
Definition - (Signed Formula).
Regular Logics.
Definition - (Circle, Corner [13]).
Definition - (Regular Logic [13]).
Definition - (Partially Ordered Set).
Definition - (Up-, Downset).
Normal Forms.
Resolution, parallel version: Definition - (Signed Subsumption).
Integer Programming.
Implementation.
Conclusion and Outlook.
References (30 publ.).