Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings
Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings
复制标题
使用分析 Tableaux 和相关方法进行自动推理 - 第 28 届国际会议，TABLEAUX 2019，英国伦敦，2019 年 9 月 3-5 日，会议记录
DOI：
10.1007/978-3-030-29026-9_19
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Docherty S
中科院分区：
文献类型：
--
作者：
Docherty S
本文定义了PDL的无穷标号微积分。然后给出了有限可表示的循环系统。我们表明，这两个是健全的和完整的PDL的标准模型，并进一步，这是切自由完成。我们还调查证明搜索策略的循环系统的PDL片段没有测试。
We define an infinitary labelled sequent calculus for PDL,. A finitarily representable cyclic system,, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, thatis cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.