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

Jie Zhang, Danwen Mao and Yong Guan

Journal of Applied Mathematics, 2013, vol. 2013, issue 1

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.

Date: 2013
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2013/218492

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2013:y:2013:i:1:n:218492

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().