一种多车道空间逻辑的证明论
计算机科学中的逻辑
2017-01-11 v2
摘要
我们扩展了多车道空间逻辑 MLSL（该逻辑在先前工作中引入，用于证明多车道高速公路上交通操纵的安全性（无碰撞）），增加了长度测量和动态模态。我们研究这一扩展（称为 EMLSL）的证明论。为此，我们证明了 EMLSL 的不可判定性，但仍然给出了一个可靠的证明系统，可用于推理交通场景的安全性。我们通过为先前只能非形式化证明的预留引理给出形式化证明来阐明后者。此外，我们证明了一个基本定理，表明长度测量独立于高速公路上的车道数。
引用
@article{arxiv.1504.06986,
title = {Proof Theory of a Multi-Lane Spatial Logic},
author = {Sven Linker and Martin Hilscher},
journal= {arXiv preprint arXiv:1504.06986},
year = {2017}
}
备注
This paper is the extended and slightly revised version of our publication in the 10th International Colloquium on Theoretical Aspects of Computing (ICTAC) in 2013