Formalization of Linear Space Theory in the Higher-Order Logic Proving System
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 s...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/218492 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832560634244366336 |
|---|---|
| author | Jie Zhang Danwen Mao Yong Guan |
| author_facet | Jie Zhang Danwen Mao Yong Guan |
| author_sort | Jie Zhang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-e494db69a70a445994ff5f8907b49947 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-e494db69a70a445994ff5f8907b499472025-02-03T01:27:11ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/218492218492Formalization of Linear Space Theory in the Higher-Order Logic Proving SystemJie Zhang0Danwen Mao1Yong Guan2College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, ChinaCollege of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, ChinaCollege of Information Engineering, Capital Normal University, Beijing 100048, ChinaTheorem 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.http://dx.doi.org/10.1155/2013/218492 |
| spellingShingle | Jie Zhang Danwen Mao Yong Guan Formalization of Linear Space Theory in the Higher-Order Logic Proving System Journal of Applied Mathematics |
| title | Formalization of Linear Space Theory in the Higher-Order Logic Proving System |
| title_full | Formalization of Linear Space Theory in the Higher-Order Logic Proving System |
| title_fullStr | Formalization of Linear Space Theory in the Higher-Order Logic Proving System |
| title_full_unstemmed | Formalization of Linear Space Theory in the Higher-Order Logic Proving System |
| title_short | Formalization of Linear Space Theory in the Higher-Order Logic Proving System |
| title_sort | formalization of linear space theory in the higher order logic proving system |
| url | http://dx.doi.org/10.1155/2013/218492 |
| work_keys_str_mv | AT jiezhang formalizationoflinearspacetheoryinthehigherorderlogicprovingsystem AT danwenmao formalizationoflinearspacetheoryinthehigherorderlogicprovingsystem AT yongguan formalizationoflinearspacetheoryinthehigherorderlogicprovingsystem |