We overview applications of Craig interpolation and Beth definability to simplifying logical expressions or database queries. From the perspective of the theory of interpolation and definability the results give a number of new angles. First, they give a different take on what it means to make definability or interpolation results effective, looking at algorithms that take a proof as input and return an interpolant or explicit definition as output. Secondly, they relate interpolation and definability to preservation theorems in model theory: interpolation and definability theorems are the basis for many "semantics-to-syntax" results, relating a semantic property of a formula to its equivalence with a certain syntactic form. Thirdly, they motivate new forms of interpolation and definability, focusing on syntactic forms that are of interest in databases.

翻译：我们概述了克雷格插值与贝斯可定义性在简化逻辑表达式或数据库查询中的应用。从插值与可定义性理论的角度来看，这些成果提供了若干新视角。首先，它们对如何使可定义性或插值结果具有有效性给出了不同诠释——考察那些以证明为输入、以插值项或显式定义为输出的算法。其次，它们将插值与可定义性关联至模型论中的保持定理：插值定理与可定义性定理是诸多"语义到语法"结果的基础，这些结果将公式的语义性质与其等价于特定语法形式联系起来。第三，它们推动了对插值与可定义性新形式的探索，重点关注数据库领域中有意义的语法形式。