ABS Golrangi (Persion)

هدف ما در اين پايان نامه مطالعه منطق اثبات ها و برخي گسترش هاي آن است. منطق اثبات ها ابتدا توسط آرتموف در سال 1994 مطرح گرديد. يكي از انگيزه هاي شكل گيري منطق اثبات ها، ارائه يك معناشناسي اثبات پذيري دقيق برايS4 و صوري كردن تعبيرBHK براي منطق شهودي بود.LP   گسترشي از منطق گزاره اي كلاسيك است كه زبان آن علاوه بر نمادهاي منطق گزاره اي شامل عملگرهاي اثبات مي باشد.

   در اين پايان نامه ضمن بيان زمينه هاي تاريخي صوري سازي اثبات ها، دستگاه LP را معرفي كرده و قضيه تماميت حسابي آن را ثابت مي كنيم. همچنين نشان مي دهيم كه LP قابليت تحقق منطق موجه   4را در خود دارد.

   يكي از گسترش هايLP منطق اثبات ها و اثبات پذيري (LPP ) است. اين دستگاه از تركيب همزمان وجه اثبات پذيري و احكام شامل ترمهاي اثبات به دست مي آيد. پس از معرفي مدلهاي كريپكي، تماميت حسابي LPP ثابت مي شود.

   در خاتمه منطق اثبات ها براي HA مطرح مي گردد. قواعد پذيرفتني در HA كه در واقع همان قواعد پذيرفتني در IPC مي باشند، در اصل بندي كامل اين دستگاه نقش مهمي دارا هستند