پديد آورنده :
قاري، مقداد
عنوان :
جنبه هايي از منطق تلفيقي اثباتها و اثبات پذيري
گرايش تحصيلي :
منطق رياضي
محل تحصيل :
اصفهان: دانشگاه صنعتي اصفهان، دانشكده علوم رياضي
صفحه شمار :
[شش]،154ص.: مصور،جدول،نمودار
يادداشت :
ص.ع.به فارسي و انگليسي
استاد راهنما :
مجتبي آقايي
استاد مشاور :
مرتضي منيري
توصيفگر ها :
منطق توجيه , منطق موجهات , قضيه تحقق , دستگاههاي گنتسني , حذف برش
تاريخ نمايه سازي :
1/8/91
استاد داور :
محمد اردشير، مسعود پور مهديان، رسول رمضانيان
كد ايرانداك :
ID457 دكتري
چكيده فارسي :
به فارسي و انگليسي: قابل رويت در نسخه ديجيتالي
چكيده انگليسي :
Aspects of the Joint Logic of Proofs and Provability Meghdad Ghari mghari@math iut ac ir June 12 2012 Doctor of Philosophy Thesis Department of Mathematical Sciences Isfahan University of Technology Isfahan 84156 83111 IranSupervisor Dr Mojtaba Aghaei aghaei@cc iut ac ir Advisor Dr Morteza Moniri m moniri@cc sbu ac ir Department Graduate Program Coordinator Dr Gholamreza Omidi romidi@cc iut ac ir Department of Mathematical Sciences Isfahan University of Technology Isfahan 84156 83111 Iran Department of Mathematics Shahid Beheshti University Tehran Iran Abstract Justi cation logics provide a framework for reasoning about epistemic justi cations Inthis thesis we study justi cation logics and their relations with modal logics The resultsof the thesis can be divided into two parts we introduce new justi cation logics and provethe realization theorem and study the proof theory of justi cation logics We introduce newjusti cation logic JB justi cation counterpart of Browerean modal logic KB and its exten sions JGL justi cation counterpart of G del L b provability logic GL JKD JTD JS4D and o o n n n D DJS5n justi cation counterpart of distributed knowledge logics L For these justi cationlogics the realization theorem are proved epistemic models are given and completeness the orems are established We prove the realization theorem for KB using embedding in anotherjusti cation logic for GL using Artemov s syntactical method and for LD using Fitting s se mantical method We also provide various proof systems for justi cation logics and prove thecut elimination theorem for most of them We present a syntactical proof of cut eliminationfor Artemov s sequent calculus LPG of the logic of proofs LP and present cut free sequentcalculi LPG and LPG for the logic of proofs cut free sequent calculi S4LPG and S4LPG for L L Hepistemic logic with justi cation S4LP cut free hypersequent calculus S4LPNL for epistemiclogic with justi cation S4LPN cut and contraction free labeled sequent calculus for most ofthe justi cation logics as well as S4LP and S4LPN Key WordsJusti cation logic Modal logic Distributed knowledge Realization theorem Sequent calcu lus Cut elimination IntroductionArtemov in 1 proposed the Logic of Proofs LP to present a provability interpretation for themodal logic S4 and intuitionistic propositional logic LP extends the language of propositionallogic by expressions of the form t A with the intended meaning term t is a proof of A Terms are constructed from variables and constants by means of operations on proofs LP canbe also viewed as a re nement of the epistemic logic S4 in which knowability operator 2A A is known is replaced by explicit knowledge operators t A t is a justi cation for A The logic of proofs LP is the rst logic introduced in the familly of justi cation log ics Various justi cation logics have been introduced so far They are connected to normal 1
استاد راهنما :
مجتبي آقايي
استاد مشاور :
مرتضي منيري
استاد داور :
محمد اردشير، مسعود پور مهديان، رسول رمضانيان
