Journal of Applied Mathematics
Volume 2013 (2013), Article ID 218492, 6 pages
http://dx.doi.org/10.1155/2013/218492
Research Article

Formalization of Linear Space Theory in the Higher-Order Logic Proving System

Jie Zhang,1 Danwen Mao,1 and Yong Guan2

1College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China
2College of Information Engineering, Capital Normal University, Beijing 100048, China

Received 8 March 2013; Accepted 1 April 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Jie Zhang et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Abstract

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.