字符串上子句的等式定理证明 Equational Theorem Proving for Clauses over Strings

作者:Dohan Kim

尽管几十年来,关于字符串上方程的推理已经得到了广泛的研究,但关于字符串上一般子句的等式推理的研究却很少。本文介绍了一种新的带字符串的叠加微积分,并提出了一个关于字符串上子句的等式定理证明框架。它为字符串上的分句提供了一个饱和过程,并证明了所提出的具有收缩规则的叠加演算是证明完备的。本文还提出了一个新的字符串上的单词问题的决策过程,w.r.t.如果在所提出的推理系统下r可以是有限饱和的,则字符串上的一组条件方程r。

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. This paper also presents a new decision procedure for word problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system.

论文链接:http://arxiv.org/pdf/2303.13257v1

更多计算机论文:http://cspaper.cn/

Related posts