Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs.

翻译：依赖对构成了一系列用于项重写系统终止性分析的高效技术。本文中，我们将静态依赖对框架适配于逻辑约束简单类型项重写系统（LCSTRSs）——一种内建逻辑约束的高阶形式化方法。同时，我们提出了通用可计算性的概念，该概念通过静态依赖对的使用，实现了一种开放世界终止性分析的形式。