سال انتشار: ۱۳۸۶

محل انتشار: ششمین همایش سراسری علوم پایه

تعداد صفحات: ۱۰

نویسنده(ها):

فردین اسماعیل نیا – دانشگاه آزاد اسلامی واحد رودهن- عضو هیات علمی دانشگاه آزاد اسلامی واح
ابوالقاسم کلانتری – دانشگاه آزاد اسلامی واحد رودهن- مدرس حق التدریس دانشگاه آزاد اسلامی و

چکیده:

این مقاله قضیه اثباتگری با کمک رایانه برای منطق های زمانی خطی ارائه می دهد و هدف آن گسترش قابلیت مشارکت کاربر و سیستم های خودکار برای اثبات قضیه در نطق های زمانی است. همچنین بر افزایش موثر مشارکت کاربر در چنین سیستم هایی تکیه می شود. به ویژه تکنیک های شناخته شده اثبات با نقطه گذاری و روش نقطه و پرتاب را که برای ساختارهای اثباتی کنترل با موشواره در منطق گزارهای وجود دارد، در منطق زمانی گسترش میدهد و نیز نشان میدهد که چگونه با داشتن ترجمه ای قبلی برای منطق گزاره ای و گسترش آن به عملگرهای زمانی میتوان یک اثبات با متن تولید کرد قضیه اثباتگر سیستمی برای منطق زمانی ارائه میدهد که قواعد استنتاج آن شهودی تر از قواعدی است که معمولاً برای منطق زمانی ارائه می شود بنابراین برای هدف مذکور مناسب ترند همچنین با مقایسه این سیستم استنتاجی با یک سیستم شناخته شده سلامت و تمامیت آن ثابت می شود.