Formalization of Linear Space Theory in the Higher-Order Logic Proving System
Joint Authors
Guan, Yong
Zhang, Jie
Mao, Danwen
Source
Journal of Applied Mathematics
Issue
Vol. 2013, Issue 2013 (31 Dec. 2013), pp.1-6, 6 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2013-04-23
Country of Publication
Egypt
No. of Pages
6
Main Subjects
Abstract EN
Theorem proving is an important approach in formal verification.
Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics.
Higher-order logic is more expressive.
This paper presents the formalization of the linear space theory in HOL4.
A set of properties is characterized in HOL4.
This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.
American Psychological Association (APA)
Zhang, Jie& Mao, Danwen& Guan, Yong. 2013. Formalization of Linear Space Theory in the Higher-Order Logic Proving System. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-6.
https://search.emarefa.net/detail/BIM-455501
Modern Language Association (MLA)
Zhang, Jie…[et al.]. Formalization of Linear Space Theory in the Higher-Order Logic Proving System. Journal of Applied Mathematics No. 2013 (2013), pp.1-6.
https://search.emarefa.net/detail/BIM-455501
American Medical Association (AMA)
Zhang, Jie& Mao, Danwen& Guan, Yong. Formalization of Linear Space Theory in the Higher-Order Logic Proving System. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-6.
https://search.emarefa.net/detail/BIM-455501
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-455501
