一句话：为归纳行为关系建立类似余归纳增强的证明理论，并以权重保持条件保证增强函数的可靠性。
余归纳证明方法已有丰富的增强理论，广泛用于互模拟等行为关系。本文研究如何为归纳行为关系（由归纳可观测量定义）建立类似理论。与余归纳情形相同，理论使用半进展 R -> F(R)：R 为进程关系，F 为关系函数，表示 R 中进程迁移可匹配且导数落入 F(R)。对给定预序，增强对应可靠函数，即 R -> F(R) 蕴含 R 包含于该预序；等价关系同理。作者为可观测量引入权重，并给出函数保持权重的条件以保证可靠性，证明该函数类包含非平凡函数且对若干函数构造子封闭，从而由简单可靠函数导出复杂证明技术。文中区分强语义与弱语义，并测试若干非平凡例子。
There exist a rich and well-developed theory of enhancements of the coinduction proof method, widely used on behavioural relations such as bisimilarity. We study how to develop an analogous theory for inductive behaviour relations, i.e., relations defined from inductive observables. Similarly to the coinductive setting, our theory makes use of (semi)-progressions of the form R->F(R), where R is a relation on processes and F is a function on relations, meaning that there is an appropriate match on the transitions that the processes in R can perform in which the process derivatives are in F(R). For a given preorder, an enhancement corresponds to a sound function, i.e., one for which R->F(R) implies that R is contained in the preorder; and similarly for equivalences. We introduce weights on the observables of an inductive relation, and a weight-preserving condition on functions that guarantees soundness. We show that the class of functions contains non-trivial functions and enjoys closure properties with respect to desirable function constructors, so to be able to derive sophisticated sound functions (and hence sophisticated proof techniques) from simpler ones. We consider both strong semantics (in which all actions are treated equally) and weak semantics (in which one abstracts from internal transitions). We test our enhancements on a few non-trivial examples.