فاطمه‌سادات نبوی
دانشگاه قم
چکیده. در این ارائه در ابتدا پارادوکس تخلف از وظیفه تبیین می‌شود که فرمال‌سازی آن رابطه تنگاتنگی با نمادین‌سازی الزامات مشروط دارد. سپس مطلوبیت‌های یک نمادین‌سازی، از منظر مواجهه با این پارادوکس بیان می‌شود.
در ادامه با اشاره به شرط ماهیتی تعریف عملگر الزام و رابطه نزدیک این مفهوم با حیطه عمل فرد و شکاف بین این مفهوم با آنچه آن را واجبات اولیه می‌خوانیم، به بیان نمونه هایی از تفکیک این دو مفهوم در پیشینه منطق تکلیف، با هدف تبیین مطلوب پارادوکس تخلف از وظیفه و یا تبیین سازگار تعارضات تکلیفی می‌پردازیم.
در ادامه پس از بیان این تفکیک در اصول فقه و ارائه یک چارچوب منطقی برای آن، شیوه بیان نمادین خود برای الزامات مشروط در این چارچوب را بیان می‌کنیم و انتظارات خود برای فرمال‌سازی واجبات مشروط را در این چارچوب می‌آزماییم.
سیداحمد میرصانعی
دانشگاه تربیت مدرس
چکیده. فرم منطقی استدلال ابداکشن هنوز هم یک سؤال باز به حساب می‌آید و نظریات گوناگونی در مورد آن ارائه شده است. ابداکشن نوعی از استدلال‌های غیریکنوا و الغاءپذیر است و منطق حاوی چنین استدلالی نیز از اقسام منطق‌های غیریکنوا و الغاءپذیر مانند منطق استقرائی است. ابداکشن نوعی استدلال طبیعی است و راهکاری است برای حل مسائلی که پدیده‌ی \(\varphi\) با تئوری \(\Theta\) تببین‌پذیر نیست و نیاز به جستجوی تبیینی برای \(\varphi\) داریم. با در نظر گرفتن \(\alpha\) به عنوان تبیین و \(\langle\Theta,\varphi\rangle\) به عنوان مسأله ابداکشنی، \(\Theta\cup\{\alpha\}\models\varphi\) فرمت منطقی یک استدلال ابداکشنی قوی است. در این مقاله ابتدا نظریه برهان برای حساب مرتبه اول ابداکشنی بر مبنای نظریه برهان مرتبه اول گنتزن طرح می‌شود. این حساب با نظر به سمانتیک تابلو دوگان آن و بدون نیاز به ترجمه فرمول‌ها به صورت نرمال، صحیح و تمام است. پس از بررسی قواعد ساختاری این حساب، به بعضی ملاحظات فرامنطقی و سؤالات باز همچون سازگاری، تمامیت و تصمیم‌ناپذیری این حساب پرداخته شده است.
-----------------------------------------------------
Proof Theory of First Order Abduction: Sequent Calculus and Structural Rules
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.
Meghdad Ghari
University of Isfahan & Institute for Research in Fundamental Sciences (IPM)
Abstract. In this paper we present tableau proof systems for proposi- tional justification logics. We show that the tableau systems are sound and complete with respect to Mkrtychev models. Some of the tableau systems are fully analytic and can be used to prove the decidability of justification logics for finite constant specifications. Finally we prove the interpolation property and Beth definability property for some of the justification logics.
Ali Farjami
University of Luxembourg
Abstract. The so-called modal logic and norm-based paradigms in deontic logic investigate the logical relations among normative concepts such as obligation, permission, and prohibition. The talk unifies these two paradigms by introducing an algebraic framework, called discursive input/output logic. In this framework, deontic modals are evaluated with reference both to a set of possible worlds and a set of norms. The distinctive feature of the new framework is the non-adjunctive definition of input/output operations. This brings us the advantage of modeling discursive reasoning.
Amir Hossein Sharafi, Asadollah Fallahi
Iranian Institute of Philosophy
Abstract. One way of investigation on properties of a class of logics, such as tabularity and pretabularity, is to describe the lattice of those logics. This investigation can be done in algebraic or relational aspects. In algebraic viewpoint, we study the properties of the lattice of corresponding varieties. This helps us to invoke general results of the algebraic theory of lattices of varieties. Tabular varieties (corresponding to tabular logics) are generated by a finite algebra and pretabular ones are those which are not tabular but their pure subvarieties are tabular. Our goal is to specify the number of pretabular subvarieties of the variety corresponding to the classical relevance logic (KR). Then we would have found the number of pretabular extensions of classical relevance logic. We also want to know the number of subvarieties of these pretabular varieties as their height. For instance, Maksimova could prove that the pretabular extensions of intuitionistic logic Int and modal logic S4 are finite (three and five, respectively) [6, 7]. But in [2] Blok showed that the number of pretabular extensions of K4 is uncountable. Although all of these logics have uncountable height [3, 2], Swirydowicz deduced that relevance logic R has uncountable pretabular extensions by finite heights [8]. Furthermore, two pretabular extensions of KR have been derived, one by Galminas and Mersch in [5] and another by Fallahi in [4]. Finding a way to estimate the number of pretabular extensions of classical relevance logic (KR) and their heights has leaded us to make a KR-frame inspiring from the recession frame introduced in [1], and the relational frame used in [8]. This KR-frame gives us the idea that there are uncountable pretabular extensions for KR with finite height.
References.
[1] Blok. W. J. The Lattice of Modal Logics: An Algebraic Investigation, the journal of smbolic logic, 45, 221-236, 1980.
[2] Blok. W. J. Pretabular Varieties of Modal Algebras, Studia Logica, 39: 101-124, 1980.
[3] A. Day, Varieties of Heyting algebras, unpublished manuscript.
[4] Fallahi, A., A Second Pretabular Classical Relevance Logic, Studia Logica, 106, pp. 191-214, 2018.
[5] Galminas, L., and J. G. Mersch, A Pretabular Classical Relevance Logic, Recent Developments related to Residuated Lattices and Substructural Logics, Studia Logica 100: 1211–1221, 2012.
[6] Maksimova, L. L., ‘Pretabular extensions of Lewis’s logic S4’, Algebra i Logika 14(1): 28–55, 1975.
[7] Maksimova, L. L., ‘Pretabular superintuitionistic logics’, Algebra i Logika 11(5): 558–570, 1972.
[8] Swirydowicz, K., There exists an uncountable set of pretabular extensions of the relevant logic R and each logic of this set is generated by a variety of finite height, The Journal of Symbolic Logic 73 (4): 1249-1270, 2008.
Nazanin Roshandel Tavana
Department of Mathematics and Computer Science, Amirkabir University of Technology
Abstract.In this paper, rational Gödel logic is introduced and some model theory for it is expressed. In this version of Gödel logic, the set of truth values is extended and also, rational numbers are added as formulas. In particular, Craig interpolation property is studied for this logic.
ریحانه ذوقی‌فرد، محمد گلشنی
پژوهشگاه دانش‌های بنیادی
Abstract. In 1990, Andreas Blass introduced a filter sequence semantic for modal logic and showed that the provability logic GL is complete with respect to the end filter sequence. He also showed that it is consistent that GL is complete with respect to the club filter and that in this case, it's incompleteness is equiconsistent with the existence of a Mahlo cardinal. He asked if it is consistent that GL is complete with respect to the normal filter sequence. In this talk, we answer the above question. Assuming the existence of suitable large cardinals, we show that it is consistent that GL is complete with respect to the normal filter sequence. This is joint work with Reihane Zoghifard.
درة‌السادات دستغیب، هادی فراهانی
گروه علوم کامپیوتر، دانشکدۀ علوم ریاضی، دانشگاه شهیدبهشتی
چکیده. در این مقاله ما یک توسیع شناختی از منطق فازی وکاشیویچ با کمک عملگر باور ارائه و برای آن یک روش معناشناسی برمبنای ساختار کریپکی ارائه می کنیم که در آن هم ارزش گزاره ها و هم ارزش رابطه های تمییز ناپذیری مقدار فازی می گیرند. در ادامه با اضافه کردن اصولی شناختی، تعدادی دستگاه استنتاجی معرفی می کنیم و در نهایت صحت و تمامیت دستگاه های استنتاجی موردنظر را نسبت به ساختارهای کریپکی مناسب اثبات می کنیم.
علیرضا دارابی
گروه فلسفه و کلام اسلامی دانشگاه آزاد اسلامی واحد علوم و تحقیقات
ادعا می‌شود که تقسیم قضایا به حقیقیه، خارجیه و ذهنیه کشفی مهم در سنت منطق سینوی است؛ شاید چنین باشد. بی‌شک در میان بحث‍‌های معاصران درباب منطق سینوی هیچ بحثی مانند این تقسیم، پردامنه و پر اختلاف نیست. با این همه یک نکته مورد اتفاق همه منطق‌دانان سنتی در دوران معاصر است: این تقسیم‌بندی هیچ تغییری در قیاس‌ها و استدلال‌های موجود در منطق سینوی ایجاد نمی‌کند؛ ادعایی که در صورت‌بندیهای مبتنی بر منطق جدید از آراء منطق‌دانان سینوی زیر سؤال رفته است.
برخی از محققین معاصر تلاش نموده‌اند که پاره‌ای از مهم‌ترین آراء موجود درباره تقسیم قضایا به حقیقیه، خارجیه و ذهنیه را صورت‌بندی کنند. همچنین تلاش‌هایی برای تحلیل و دفاع از قیاس‌های موجه نزد ابن‌سینا با بهره‌گیری از صورت‌بندیهای منطق جدید انجام گرفته است. در این تحلیل‍ها قضایای موجبه کلیه به شکلی صورت‌بندی شده‌اند که موافق با درک کلی معاصرین از قضایای حقیقیه، دارای جهت ضرورت به عنوان جهت سوراست. با این همه در مجموعه این تلاش‌ها تنها به بررسی قیاس‌های موجهاتی بسنده شده است. راقم این سطور تلاش نموده است این صورت‌بندی را به بقیه قیاس‌های موجود در آثار ابن‌سینا و به ویژه قیاس‌هایی با مقدمات شرطی بسط دهد.
شرطی در آثار ابن‌سینا شکلی ویژه دارد. شرطی در سنتی که ابن‌سینا پایه نهاده است دارای سور است. این نگاه تعداد قیاس‌های با مقدمات شرطی را بسیار افزایش می‌دهد. در مجموعه‌ای از این قیاس‌ها یکی از مقدمات شرطی و دیگری حملی است. بر پایه تحلیل سور شرطی‌ها با استفاده از ابزار جهان‌های ممکن می‌توان نشان داد که در همه مقدمات حملی استفاده شده در این قیاس‌ها، مقدمه حملی نیازمند جهت ضرورت به عنوان جهت سور خواهد بود. بدین ترتیب قیاس‌های موجود در منطق ابن سینا تنها با حقیقیه دانستن مقدمات حملی قابل دفاع خواهند بود. همچنین اگر مرجعیت نگاه ابن‌سینا را برای بررسی قضایای حقیقیه بپذیریم، تحلیل مورد بحث می‌تواند مبنایی برای قضاوت درباب بخشی از نزاع‍های موجود درباره قضایای حقیقیه، خارجیه و ذهنیه باشد. با این همه این تحلیل نیز چندان بی‌عیب نیست چراکه در چنین نگاهی باید نسبتهای میان قضایای حقیقیه، خارجیه و ذهنیه و به ویژه نسبت تناقض بازتعریف شود.
.
Seyed Mohammad Amin Khatami
Department of Computer Science, Birjand University of Technology
Abstract. One of the nice properties of the first-order logic is the compactness of satisfiability. It states that a finitely satisfiable theory is satisfiable. Here, some new results are given around the compactness of satisfiability in Hájek Basic logic. It is shown that there are topologies on [0, 1] and [0, 1]2 for which the interpretation of all logical connectives of the Basic logic are continuous. Furthermore, a topology on first-order structures is introduced for any similarity relation, and then by the same ideas as in the continuous logic, the results around the compactness of satisfiability for Basic logic are extended.
Amirhoshang Hoseinpour Dehkordi
School of Computer Science, Institute for Research in Fundamental Sciences
| Majid Alizadeh | Ali Movaghar | |
| School of Mathematics, Statistics and Computer Science College of Science | Department of Computer Engineering, Sharif University of Technology |
Abstract. Current applied intelligent systems have crucial shortcomings either in reasoning the gathered knowl- edge, or representation of comprehensive integrated information. To address these limitations, we develop a formal transition system, which is applied to classifiers (the common artificial intelligence (AI) systems), to reason about the findings. The developed model was created by combining the Public Announcement Logic (PAL) and the Linear Temporal Logic (LTL), which will be done to analyze both single-framed data and the following time-series data. To do this, first, the achieved knowledge by a classifier for an individual single-framed data will be taken, and then, it would be modeled by a PAL. Alongside the PAL, all the time-series knowledge changes will be modeled, using an LTL. This will integrate the information of the recognized input data, rules, and knowledge. As an application, assume that we have a video stream and some questions about the video. By translating the natural language questions into the temporal formulas, this model could resolve a question answering system. Finally, we suggest a mechanism to reduce the investigated paths for the performance improvements, in semi-continues data-streams. Besides, this approach would perform a partial correction for such an object-detection system. The LTPAL model leads to developing a unified representation of knowledge, and the smoothness in the integration of the gathered and external experiences. Therefore, using LTPAL, the model could receive the classifiers’ predefined -or any external- knowledge, to assemble them in a unified manner. Herein, we will develop a reasoning model on the top of a preexisted intelligent system, to reason about the knowledge, in the following steps:
- First of all, we are going to collect all the intelligent system’s possible answers. Therefore, because of the statistical nature of most classifiers, and the fact that the accuracy is based on the architecture and training set, this kind of classifier could not guarantee full accuracy. To overcome this problem, Huang et al. [1] presented an approach to verify predefined properties for each input (point-wise verification) in such models. If the input point is verified, the single and verified output would be demonstrated. Otherwise, and in the case that the property could not be verified, Dehkordi et al. [2] developed a multi-agent epistemic logic model to find all possibleA PREPRINT - J ANUARY 10, 2021 outcomes concerning that property. By applying this step, the outcome of such classifiers would be a set of all possible outputs (i.e., possible worlds).
- Generally, the set of knowledge is directly driven by classifiers, from the possible worlds. This set of knowledge for input and a system of intelligent agents contains all possible output classes, yet from a real-world perspective, each class of objects would contain more information (i.e., ontology rules). To reflect this, an intelligent agent should understand the category of the object together with sub-categories which are fed in as input rules. In this step of the model, for each possible class of object, predefined inferences would be extracted in a unified and formal manner.
- The previously developed model was exclusively designed for single-framed data, therefor the time-series data could not be considered until this step. To bring them into consideration, we developed a combination of temporal logic transition systems Gerth et al. [3] with the developed epistemic logic model. Let each frame of time-series data, as an input. After execution of the above steps on all frames, we have a set of extracted knowledge (in form of possible worlds) for each single-framed data of the input time-series data. By placing the possible worlds in hierarchical order, a transition system could be created. This leads us to extract all possible sequences (named execution path) of knowledge represented in time-series data.
- Here, we will develop an approach to use our model for a question-answering application. Accordingly, to get an outcome from the developed model, it should provide answers to questions. To do this, first, using preexisted approaches, natural language statements will be translated into temporal formulas. Then, all possible answers (in the shape of a formula) would be extracted due to the asked question (which is translated to a formula). Finally, each formula of every possible answer would be investigated in the developed temporal model and the satisfying formula reflects the answers to the question.
- The verification in this transition system is also defined by modifying the verification definition in Huang et al. [1] and Dehkordi et al. [2]. Accordingly, the situation of the answer would be determined, in other words, it is checked whether it is a verified answer, possible answer, or it by adding some missing information it would be a possible/verified answer.
- The space state explosion, and following that, numerous execution paths could make the proposed method very time and space consuming in large models. To overcome that difficulty, an approach is also developed, to find the most probable path and investigate the satisfaction on that path. This method for finding the most probable path could be lead us to a data-stream correction (if there are misclassifications in small fractions of such data), in semi-continuous data-streams.
References.
[1] Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pages 3–29, 2017.
[2] Amirhoshang Hoseinpour Dehkordi, Majid Alizadeh, Ebrahim Ardeshir-Larijani, and Ali Movaghar. Masks: A multi-classifier’s verification approach, 2020.
[3] Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In International Conference on Protocol Specification, Testing and Verification, pages 3–18. Springer, 1995.
عامر آمیخته
چکیده. در اين خلاصه‌ی مقاله، نسخه های فازی منطق‌های موجهات R و K را بر پايه منطق تكنرم UL با زبان استاندارد معرفی میكنيم. اين معرفی از طريق حساب ابررشتههای برچسبخورده بر مبنای معناشناسی استاندارد منطق موجهات صورت مي‌گيرد.
1 / 2