سیداحمد میرصانعی

‫دانشگاه تربیت مدرس

چکیده. ‫فرم منطقی استدلال ابداکشن هنوز هم یک سؤال باز به حساب می‌آید و نظریات گوناگونی در مورد آن ارائه شده است. ابداکشن نوعی از استدلال‌های غیریکنوا و الغاءپذیر است و منطق حاوی چنین استدلالی نیز از اقسام منطق‌های غیریکنوا و الغاءپذیر مانند منطق استقرائی است. ابداکشن نوعی استدلال طبیعی است و راهکاری است برای حل مسائلی که پدیده‌ی \(\varphi\) با تئوری \(\Theta\) تببین‌پذیر نیست و نیاز به جستجوی تبیینی برای \(\varphi\) داریم. با در نظر گرفتن \(\alpha\) به عنوان تبیین و \(\langle\Theta,\varphi\rangle\) به عنوان مسأله ابداکشنی، \(\Theta\cup\{\alpha\}\models\varphi\) فرمت منطقی یک استدلال ابداکشنی قوی است. در این مقاله ابتدا نظریه برهان برای حساب مرتبه اول ابداکشنی بر مبنای نظریه برهان مرتبه اول گنتزن طرح می‌شود. این حساب با نظر به سمانتیک تابلو دوگان آن و بدون نیاز به ترجمه فرمول‌ها به صورت نرمال، صحیح و تمام است. پس از بررسی قواعد ساختاری این حساب، به بعضی ملاحظات فرامنطقی و سؤالات باز همچون سازگاری، تمامیت و تصمیم‌ناپذیری این حساب پرداخته شده است.

-----------------------------------------------------

Proof Theory of First Order Abduction: Sequent Calculus and Structural Rules

Eighth Annual Conference of Iranian Association for Logic (Ial) (2021)

Abstract:
The logical formalism of abductive reasoning is still an open discussion and various theories have been presented about it. Abduction is a type of non-monotonic and defeasible reasonings, and the logic containing such a reasoning is one of the types of non-nonmonotonic and defeasible logics, such as inductive logic. Abduction is a kind of natural reasoning and it is a solution to the problems having this form "the phenomenon of φ cannot be explained by the theory of Θ" and we need to search for (or to adduce) an explanation for φ. Taking α as the explanation and <Θ,φ> as the abductive problem, Θ∪{α}⊨φ is the logical format of a strong abductive reasoning. In this article, the proof theory for first-order abductive calculus is proposed based on Gentzen-type first-order proof theory. Considering its dual, i.e., the semantic tableaux, and without the need to translate the formulas, this calculation is sound and complete. After examining the structural rules of this calculus, some metalogical considerations and open problems such as consistency, completeness and undecidability of this account have been addressed.
 
Keywords: First order Abduction Abductive Problem Proof theory sequent calculus Tableau semantics Structural rules