بلاگ

استنتاج درباره افعال

دو عامل ما را به ادغام منطق‌های توصیف و فرمالیسم‌های فعل و استدلال در هستان نگارهای پویا و پایگاه‌های دانش و فعل (KAB) سوق می‌دهد: «تقاضا برای بازنمایی و استدلال درباره خدمات وب معنایی» و «این واقعیت که شکاف بیانی بین فرمالیسم های کنشی موجود وجود دارد.».
برای بازنمایی و استدلال در مورد افعال، می‌توانیم افعال را در منطق توصیف مانند DALCO@ بپذیریم. در این منطق، اقدامات به عنوان شهروندان در نظر گرفته می شوند و علاوه بر TBox و ABox پویا، یک ActBox نیز داریم. TBox در اینجا «وضعیت‌ها»، «پیش‌شرط‌ها» و «اثرات افعال اتمی» را توصیف می‌کند و ActBox شامل مجموعه محدودی از افعال اتمی است.
اما آیا می‌توانیم الگوریتمی پایان‌پذیر و صحیح برای بررسی ارضاپذیری قضایا و استعلام از مبانی دانش و فعل داشته باشیم؟ چنین الگوریتمی باید به طور مؤثر بسیاری از وظایف استدلالی را بر روی اقدامات انجام دهد و 4 مشکل مهم را حل کند: تحقق پذیری، اجرا، طرح ریزی، مسائل برنامه ریزی.
در طول دو دهه گذشته، الگوریتم‌هایی برای تابلوی منطق پویا توصیفی پیشنهاد شده‌اند (به ویژه، چانگ و همکاران (2007)). اما به دلیل پیچیدگی محاسباتی بالا که گاهی اوقات بیش از EXPTIME و حتی NEXPTIME است، در پیاده سازی هستان نگارهای پویا با مشکلات زیادی مواجه هستیم. در تیم برهان به دنبال حل این مشکل و ارائه الگوریتم‌هایی برای پیاده‌سازی منطق پویای توصیفی در هستان نگارهای توصیفی پویا هستیم.