Formalization of Function Matrix Theory in HOL
المؤلفون المشاركون
Wei, Hongxing
Liu, Zhenke
Ye, Shiwei
Zhang, Jie
Guan, Yong
Shi, Zhiping
المصدر
Journal of Applied Mathematics
العدد
المجلد 2014، العدد 2014 (31 ديسمبر/كانون الأول 2014)، ص ص. 1-10، 10ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2014-07-24
دولة النشر
مصر
عدد الصفحات
10
التخصصات الرئيسية
الملخص EN
Function matrices, in which elements are functions rather than numbers, are widely used in model analysis of dynamic systems such as control systems and robotics.
In safety-critical applications, the dynamic systems are required to be analyzed formally and accurately to ensure their correctness and safeness.
Higher-order logic (HOL) theorem proving is a promise technique to match the requirement.
This paper proposes a higher-order logic formalization of the function vector and the function matrix theories using the HOL theorem prover, including data types, operations, and their properties, and further presents formalization of the differential and integral of function vectors and function matrices.
The formalization is implemented as a library in the HOL system.
A case study, a formal analysis of differential of quadratic functions, is presented to show the usefulness of the proposed formalization.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Shi, Zhiping& Liu, Zhenke& Guan, Yong& Ye, Shiwei& Zhang, Jie& Wei, Hongxing. 2014. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-453960
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Shi, Zhiping…[et al.]. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics No. 2014 (2014), pp.1-10.
https://search.emarefa.net/detail/BIM-453960
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Shi, Zhiping& Liu, Zhenke& Guan, Yong& Ye, Shiwei& Zhang, Jie& Wei, Hongxing. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-453960
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-453960
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر