一句话：提出对齐完备性概念，用归纳断言法与乘积自动机刻画关系霍尔逻辑的规则完备性。
关系霍尔逻辑（RHL）用于推理程序之间的关系。已有若干 RHL 包含顺序乘积规则，可从普通霍尔逻辑（HL）的判定导出关系正确性判定；其他规则虽实用，但顺序乘积本身与 HL 已相对完备。为更合理地评价 RHL，本文引入“对齐完备性”，基于归纳断言方法与乘积自动机给出定义。作者对若干不同规则集给出了对齐完备性结果，说明这些规则组合能够覆盖哪些对齐模式下的关系推理，并讨论该概念对设计更丰富编程语言的 RHL 与关系验证器的指导意义。
Relational Hoare logics (RHL) provide rules for reasoning about relations between programs. Several RHLs include a rule we call sequential product that infers a relational correctness judgment from judgments of ordinary Hoare logic (HL). Other rules embody sensible patterns of reasoning and have been found useful in practice, but sequential product is relatively complete on its own (with HL). As a more satisfactory way to evaluate RHLs, a notion of alignment completeness is introduced, in terms of the inductive assertion method and product automata. Alignment completeness results are given to account for several different sets of rules. The notion may serve to guide the design of RHLs and relational verifiers for richer programming languages and alignment patterns.