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, 1-6

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)
http://downloads.hindawi.com/journals/JAM/2013/218492.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2013/218492.xml (text/xml)

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:hin:jnljam:218492

DOI: 10.1155/2013/218492

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().