Formalization of function matrix theory in HOL

DOI10.1155/2014/201214zbMath1442.68258OpenAlexW1992678654WikidataQ59050246 ScholiaQ59050246MaRDI QIDQ2294128

Hongxing Wei, Shiwei Ye, Jie Zhang, Zhiping Shi, Yong Guan, Zhen-ke Liu

Publication date: 10 February 2020

Published in: Journal of Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1155/2014/201214

Mathematics Subject Classification ID

Matrices over function rings in one or more variables (15A54) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (4)

Formal analysis of the kinematic Jacobian in screw theory ⋮ Formal kinematic analysis of a general 6R manipulator using the screw theory ⋮ The formalization of discrete Fourier transform in HOL ⋮ Formalization of functional variation in HOL Light

Uses Software

• Isabelle/HOL
• HOL
• Flyspeck

Cites Work

• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• The gauge integral theory in HOL4
• Flyspeck II: The basic linear programs
• A family of dynamic description logics for representing and reasoning about actions
• Proof System for Applied Pi Calculus
• Formally Verified Conditions for Regularity of Interval Matrices
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics

This page was built for publication: Formalization of function matrix theory in HOL