Automated thorem proving an overview Talal H MaghrabiThe Arabian journal for science and engineering المجلة العربية للعلوم والهندسة Univeristy of Petroleum and MineralsVol 22 no 2B (October 1997) p p 245258Maghrabi Talal H
الملخص:
Automated Theorem provers are computer programs written to prove or help in proving mathematical and nonmathematical theorems Automated Theorem Proving (ATP) is a rapidly advancing field and contains many potential research areas This paper is an overview of this important field It starts by giving the needed mathematical background followed by an overview The overview includes historical background basic terminology and notations and a description of the major components of a typical theorem prover The paper also outlines the current state of research in ATP and a brief description of some of the existing theorem prover تستخدم نظم إثبات النظريات آليا في المساعدة في إثبات النظريات الرياضية وغير النظرية ويلاحظ سرعة التقدم والتطور في مجالات البحوث المتشعبة المتعلقة بإثبات النظريات آليا يقدم هذا البحث دراسة شاملة لهذا المجال المهم حيث يستعرض الخلفية الرياضية اللازمة لفهم الموضوع، كما يقدم عرضا تاريخيا لمراحل تطور البحوث في هذا المجال ويتطرق البحث إلى المصطلحات الأساسية والرموز المستخدمة ويقدم وصفا للعناصر الأساسية التي يجب أن تتوفر في نظم إثبات النظريات ويغطي البحث نبذة البحوث الحالية الجارية في مجال إثبات النظريات آليا مع إعطاء وصف مختصر لبعض النظم المتوفرة حاليا
