اثبات قضیه گزاره ای در هوش مصنوعی AI

اثبات قضیه گزاره ای در هوش مصنوعی AI

میدانید که چگونه میتوان "ایجاب" را از طریق بازرسی مدل تعیین کرد : شمارش مدل ها و نشان دادن جملاتی که باید در تمام مدلها وجود داشته باشند. در این پست نشان میدهیم که ایجاب چگونه میتواند از طریق اثبات قضیه انجام شود. منظور از اثبات قضیه، اجرای مستقیم قوانین استنتاج بر روی دستورات موجود در پایگاه دانش منطق گزاره ای هوش مصنوعی برای اثبات جمله مطلوب، بدون استفاده از مدل است. اگر تعداد مدلها زیاد ولی طول اثبات کوتاه باشد آنگاه اثبات قضیه میتواند کارآمدتر از بازرسی مدل باشد.

قبل از پرداختن به جزئیات الگوریتم "اثبات قضیه" نیاز به مفاهیمی درباره ی ایجاب داریم.

► مفهوم اول هم ارزی منطقی است : دو جمله α و β در صورتی از نظر منطقی هم ارز هستند که در مجموعه ای یکسان از مدلها درست باشند. هم ارزی منطقی α و β را به صورت β  Ξ α   مینویسیم. نقش این هم ارزی ها در منطق مثل نقش همانی های حسابی در ریاضیات است. تعریف دیگر هم ارزی به این صورت است: دو جمله α و β در صورتی هم ارز هستند که هر یک از آنها بر دیگری دلالت کند.

► مفهوم دیگر مرتبط با استلزام، اعتبار است. جمله در صورتی معتبر است که در تمام مدلها درست باشد. برای مثال جمله  p v ¬p معتبر است. جملات معتبر را جملات همیشه درست یا راستگو نیز مینامند. ، آنها الزاما درست هستند. چون جمله True در تمام مدلها درست است، هر جمله ی معتبر، هم ارز منطقی True است.

اهمیت جملات معتبر چیست؟ با توجه به تعریف ایجاب، میتوانیم به قضیه قیاس (یا قضیه استنباط) برسیم که برای یونان قدیم شناخته شده بود:

"برای هر جمله α و β داریم، α بر β دلالت میکند، اگر و فقط اگر جمله  α → β معتبر باشد."

بنابراین برای هر تصمیم گیری راجع به دلالت α بر β بررسی میکنیم که آیا (α → β) در هر مدلی درست است یا خیر. این همان کاری است که الگوریتم استنتاج انجام میدهد. یا اثبات میکنیم که (α → β) هم ارز True است. برعکس قضیه قیاس میگوید که هر جمله ایجابی معتبر، یک استنتاج قانونی و درست را توصیف میکند.

► آخرین مفهوم مورد نیاز ، قابلیت ارضا شدن است. جمله در صورتی ارضا شدنی است که در بعضی مدلها درست باشد یا توسط بعضی از مدلها ارضا شود. "قابلیت ارضا شدن" میتواند با شمارش مدلهای ممکن بازرسی شود، تا مدلی پیدا شود که این جمله را ارضا کند. مسئله تعیین قابلیت ارضا شدن جملات در منطق گزاره ها، (یعنی مسئله SAT) اولین مسئله ای است که اثبات شد، NP کامل است.

البته خاصیت های اعتبار و قابلیت ارضا شدن، مرتبط هستند : α معتبر است اگر و فقط اگر ¬α ارضا شدنی نباشد. برعکس α ارضاپذیر است اگر و فقط اگر ¬α معتبر نباشد. همچنین نتیجه مفید زیر را نیز داریم:

" α بر β دلالت میکند، اگر (αʌ¬β) ارضا شدنی نباشد."

اثبات β از α با بازرسی قابلیت ارضا شدن (αʌ¬β) دقیقا متناظر با تکنیک استاندارد اثبات ریاضی تکنیکی به نام کاهش به پوچ است. این اثبات، اثبات از طریق تکذیب یا برهان خلف نام دارد.

فرض میشود β نادرست است و نشان میدهیم که با اصول موضوعی شناخته شده α تناقض دارد. این تناقض مثل این است که بگوییم (αʌ¬β) ارضاپذیری نیست.