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

سال انتشار: 1386
نوع سند: مقاله کنفرانسی
زبان: فارسی
مشاهده: 782

فایل این مقاله در 10 صفحه با فرمت PDF قابل دریافت می باشد

استخراج به نرم افزارهای پژوهشی:

لینک ثابت به این مقاله:

شناسه ملی سند علمی:

NCSCIE06_070

تاریخ نمایه سازی: 11 شهریور 1391

چکیده مقاله:

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

نویسندگان

فردین اسماعیل نیا

دانشگاه آزاد اسلامی واحد رودهن- عضو هیات علمی دانشگاه آزاد اسلامی واح

ابوالقاسم کلانتری

دانشگاه آزاد اسلامی واحد رودهن- مدرس حق التدریس دانشگاه آزاد اسلامی و

مراجع و منابع این مقاله:

لیست زیر مراجع و منابع استفاده شده در این مقاله را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود مقاله لینک شده اند :
  • I-Felty, A.specifying and im plementing theorem provers in a higher-order ...
  • Bertot, Y. Kahn, G. thery, L. Proof by pointing, Theoretical ...
  • Felty, AThery, L. Interactive theorem proving with temporal lagic, Symbolic ...
  • Paulson, L.C. Isabelle: A generic theorem prover, Springer- Verlag LNCS, ...
  • Bastin, D. Mathews, S. Vigano, L.A modular presentation of modal ...
  • نمایش کامل مراجع