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

الملخص 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.