带终态模态逻辑的增量式最坏情况最优判定过程的正确性
计算机科学中的逻辑
2012-09-07 v1
摘要
我们提出了一种简单的理论，用于解释带终态模态逻辑的增量式且最坏情况最优判定过程的构造及其正确性。该过程对 Gor\'e 和 Widmann 的 PDL 证明器的重要方面进行了抽象描述。从输入公式开始，该过程构建一个 Pratt 风格的图表，直到该图表证明或证伪公式的可满足性。由于公式的可满足性和不可满足性通常可以通过小型图表来确定，该过程为实用证明器提供了基础。
引用
@article{arxiv.1209.1248,
title = {Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities},
author = {Mark Kaminski and Gert Smolka},
journal= {arXiv preprint arXiv:1209.1248},
year = {2012}
}
备注
11 Feb 2011, 18 pages