Search In this Thesis
   Search In this Thesis  
العنوان
Automatic proof editor for martin-­loFs type teory /
المؤلف
Naghamish, Ahmed Al­Hussein Al­Sayed Megahed.
هيئة الاعداد
باحث / أحمد الحسين السيد مجاهد نغميش
مشرف / طاهر توفيق حمزة
مشرف / سيدهم فرج تادرس
مناقش / إبراهيم فرج عبدالرحمن
مناقش / إسماعيل عمرو إسماعيل
الموضوع
Martin­L.
تاريخ النشر
2004.
عدد الصفحات
243 p. :
اللغة
الإنجليزية
الدرجة
الدكتوراه
التخصص
النظرية علوم الحاسب الآلي
تاريخ الإجازة
01/01/2004
مكان الإجازة
جامعة المنصورة - كلية العلوم - Mathematics department
الفهرس
Only 14 pages are availabe for public view

from 274

from 274

Abstract

In this work, we represent our system AutoPESM. This system is implemented using PROLOG language to be the core of interactive language. Users using this language specify the problem as a specification and the computer display the program which solve the problem. ?This thesis consists of five chapters, conclusion and future work, seven appendices, English and Arabic summaries and then references. In chapter (1) we give a general introduction to this thesis, a brief account of the history of the type theory, and the aim of this field in computer sciences. In chapter (2) we explain the expression theory in general and then display the expressions and judgements syntax in BNF form. In chapter (3) we display the Martin­L?f?s inference rules and computation rules. In chapter (4) we describe our system. We present the names of the source files of this system together with theexecutable file and how to prepare the latter through the PROLOG language. We also indicate the idea and the steps on which the AutoPESM system depends. We provide a detail user?s guide provided with illustrations of the shapes of screens with a view to make a good use of the AutoPESM system. In chapter (5) we display applications using our system. The applications cover all the purpose of our system. After that we find the conclusion and future work. In Appendices we indicate the whole parts of the system in PROLOG language.