Satisfying KBO Constraints
Satisfying KBO Constraints
复制标题
满足 KBO 约束
DOI：
10.1007/978-3-540-73449-9_29
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Middeldorp
中科院分区：
文献类型：
--
作者：
Harald Zankl;A. Middeldorp
本文提出了两种新的方法来有效地证明具有Knuth-Beneficiary阶的重写系统的终止性。权函数和优先级的约束编码在（伪）命题逻辑和由此产生的公式进行测试的可满足性。任何令人满意的分配表示权重函数和优先级，使得所诱导的Knuth-Benidorm顺序将编码重写系统的规则从左到右定向。
This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in (pseudo-)propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such that the induced Knuth-Bendix order orients the rules of the encoded rewrite system from left to right.
偏序约束的高效 BDD 编码及其在软件验证专家系统中的应用
DOI：
--
发表时间：
2004
期刊：
Lecture Notes in Artificial Intelligence 3029
影响因子：
--
作者：
M.Kurihara;H.Kondo
通讯作者：
H.Kondo