一句话：用结构归纳重构 Spacer，统一 Spacer 与 GPDR，并分析其反驳完备性问题。
约束 Horn 子句可满足性问题是许多自动验证方法的核心，而 Spacer 是其中最高效的求解器之一。Spacer 的标准描述基于抽象迁移系统，将整个过程拆成细小规则，虽便于理解单条规则，却难以从整体上讨论该过程；论文指出其声称的反驳完备性实际上因若干原因并不成立，其中一些问题在原版中不存在而是后续添加的，同时也难以把握 Spacer 与 GPDR 等过程的差异。本文提出一种由结构归纳定义的 Spacer 式过程：先归纳地形式化待解问题，给出朴素求解器，再变换得到 Spacer 式过程。有趣的是，该归纳方法几乎统一了 Spacer 与 GPDR，二者在其中仅有一处不同。作者还以此框架审视文献中的 Spacer 变体，解释其为何不具备反驳完备性以及如何修复，并实现了所提过程进行实验评估。
The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and S pacer is one of the most efficient solvers of this problem. The standard description of S pacer is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between S pacer and another procedure, such as GPDR. This paper aims to provide a better understanding of S pacer by developing a S pacer -like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naive solver and transform it to obtain a S pacer -like procedure. Interestingly, our inductive approach almost unifies S pacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding S pacer , we examine S pacer variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.