更改

=== 包容与统一 ===

=== 包容与统一 ===

约束建模理论关注由'''偏序 partial order'''关联的有向图族。在这些应用中，图是按特异性排序的，这意味着更具体并因此包含更多信息的约束图被更一般的图所包含。 图之间的运算包括计算两个图（如果有的话）之间包容关系的方向，以及计算图的统一性。两个参数图的统一定义为与输入一致（即包含所有信息）的最一般的图（或其计算）（如果存在的话）；有效的统一算法是已知的。

约束建模理论关注由偏序 partial order关联的有向图族。在这些应用中，图是按特异性排序的，这意味着更具体并因此包含更多信息的约束图被更一般的图所包含。 图之间的运算包括计算两个图（如果有的话）之间包容关系的方向，以及计算图的统一性。两个参数图的统一定义为与输入一致（即包含所有信息）的最一般的图（或其计算）（如果存在的话）；有效的统一算法是已知的。

对于严格组合 compositional的约束框架，图的统一是充分可满足性和组合函数。 著名的应用包括'''定理自动证明 automatic theorem proving'''和语言结构的精化建模。

对于严格组合 compositional的约束框架，图的统一是充分可满足性和组合函数。 著名的应用包括'''定理自动证明 automatic theorem proving'''和语言结构的精化建模。

=== 路径问题 ===

=== 路径问题 ===