اثبات قضیه در منطق های زمانی به کمک رایانه و کاربر

Abstract

هدف این مقاله توصیفی، آشناکردن علاقه مندان با نمونه هایی از تلاش هایی است که در جهت استفاده از سیستم های منطقی برای ماشینی سازی اثبات در دست انجام است. اهداف این مقاله عبارتند از (1) ارائه الگوریتیم که با استفاده از ایده کاربر و ادامه روند اثبات توسط رایانه، اثباتی در سیستم گنسنی ارائه دهد. (2) ارائه الگوریتمی که با استفاده از ایده کاربر و ادامه اثبات با رایانه، اثباتی متنی در سیستم استنتاج طبیعی ارائه دهد. به معرفی سیستم های گنسنی برای منطق موجه و تکنیک های اثبات به روش نقطه و پرتاب می پردازیم و در انتها با استفاده از زبان شبه طبیعی، روش تولید چنین اثباتهایی را به کمک رایانه و کاربر ارائه می کنیم.