Formal Proof of a Machine Closed Theorem in Coq
المؤلفون المشاركون
You, Zhiyang
Zhao, Xibin
Wan, Hai
He, Anping
المصدر
Journal of Applied Mathematics
العدد
المجلد 2014، العدد 2014 (31 ديسمبر/كانون الأول 2014)، ص ص. 1-9، 9ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2014-03-30
دولة النشر
مصر
عدد الصفحات
9
التخصصات الرئيسية
الملخص EN
The paper presents a formal proof of a machine closed theorem of TLA+ in the theorem proving system Coq.
A shallow embedding scheme is employed for the proof which is independent of concrete syntax.
Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform.
A useful proof pattern of constructing a trace with desired properties is devised.
A number of Coq reusable libraries are established.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Wan, Hai& He, Anping& You, Zhiyang& Zhao, Xibin. 2014. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-505961
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Wan, Hai…[et al.]. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics No. 2014 (2014), pp.1-9.
https://search.emarefa.net/detail/BIM-505961
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Wan, Hai& He, Anping& You, Zhiyang& Zhao, Xibin. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-505961
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-505961
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر