KeYmaera X 证明 IDE——混合系统定理证明中的可用性概念
计算机科学中的逻辑
2017-01-31 v1 人机交互
编程语言
摘要
混合系统验证对于开发物理系统的正确控制器非常重要，但也具有挑战性。因此，验证工程师需要被赋予引导混合系统验证的方法，同时尽可能从自动化获得帮助。由于不可判定性，验证工具需要充分的手段在验证过程中进行干预，并需要允许验证工程师提供系统设计见解。本文介绍了混合系统定理证明器 KeYmaera X 的用户界面背后的设计理念。我们讨论它们如何使证明混合系统更容易，并首先帮助学习如何进行证明。毫不意外，最困难的用户界面挑战源于集成自动化与人类引导的渴望。我们还分享了关于此类用户界面设计成功与否如何评估的思考以及相关的轶事观察。
引用
@article{arxiv.1701.08469,
title = {The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving},
author = {Stefan Mitsch and André Platzer},
journal= {arXiv preprint arXiv:1701.08469},
year = {2017}
}
备注
In Proceedings F-IDE 2016, arXiv:1701.07925