逆方法实现模态满足性的自动机方法

基于表格法的模态逻辑和描述逻辑满足性判定程序在实际应用中表现良好，但对于获取这些方法的精确最坏情况复杂度结果有时会感到困难，尤其是对于EXPTIME-complete的逻辑。相比之下，基于自动机的方法往往可以轻易获得能够轻证明最优最坏情况复杂度的算法。然而，这些方法通常得到的算法不仅是最坏情况指数级的：它们首先构造一个始终以输入大小为指数的自动机，然后对这个大型自动机应用（多项式）的空性测试。为克服这一问题，必须尝试在执行空性测试的同时“即时”构造自动机。本文将展示，Voronkov的逆方法可被视为模态逻辑K的自动机方法所实现的空性测试的即时实现。本结果的优势体现在两个方面：首先，它表明Voronkov对逆方法的实现——该实现在实际中表现良好——是自动机方法K的满足性判定程序的优化即时实现。其次，它可用于给出Voronkov的优化不破坏程序完备性的更简洁的证明。我们还将展示逆方法可以轻易扩展以处理全局公理，以及在此设置下与自动机方法之间的对应关系仍然成立。特别是，逆方法为模态逻辑K中针对全局公理的满足性提供了一个EXPTIME算法。