Isabelle/HOL中物理量、单位与测量的自动推理
计算机科学中的逻辑
2023-02-16 v1
摘要
信息物理与机器人系统的形式化验证要求我们能精确建模现实世界中存在的物理量。在此类物理量中显式使用单位可带来更高程度的严谨性,因为可确保计算中量的兼容性。同时,单位的误用可能成为安全的障碍,因此极需在物理计算中具备自动健全性检查。本文中,我们在Isabelle/HOL中给出了国际量制(ISQ)及关联SI单位制的机械化。我们展示了如何将Isabelle用于为物理量提供类型系统及自动证明支持。物理量由维度类型(对应于基向量)参数化,从而仅有同维度的量可被等同。由于底层的“量的代数”在量与SI类型上诱导同余,我们开发了特定策略支持以捕捉这些同余。我们的构造通过一组已知的量与SI单位间等价性的测试集得以验证。此外,所提理论可用于SI制与其他制式(如英制单位制(BIS))间类型安全的转换。
引用
@article{arxiv.2302.07629,
title = {Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL},
author = {Simon Foster and Burkhart Wolff},
journal= {arXiv preprint arXiv:2302.07629},
year = {2023}
}
备注
10 pages, submitted to ICECCS 2023