Iterative Specialisation of Horn Clauses
Iterative Specialisation of Horn Clauses
复制标题
Horn 子句的迭代特化
DOI：
10.1007/978-3-540-78739-6_11
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
H. R. Nielson
中科院分区：
文献类型：
--
作者：
Christoffer Rosenkilde Nielsen;F. Nielson;H. R. Nielson
我们提出了一种通过迭代专业化解决 Horn 子句的通用算法。该算法是通用的，因为它可以用 Horn 子句的任何可判定片段进行实例化，从而产生保证健全性和终止性的通用 Horn 子句的解决方案，此外，它提供了足够的完整性标准。然后，我们通过创建一个基于可判定类 H1 的实例来演示该框架的使用，该实例能够解决基于 Yahalom 协议的重要协议分析问题。
We present a generic algorithm for solving Horn clauses through iterative specialisation. The algorithm is generic in the sense that it can be instantiated with any decidable fragment of Horn clauses, resulting in a solution scheme for general Horn clauses that guarantees soundness and termination, and furthermore, it presents sufficient criteria for completeness. We then demonstrate the use of the framework, by creating an instance of it, based on the decidable class H1, capable of solving a non-trivial protocol analysis problem based on the Yahalom protocol.