一句话:提出通用自动机理论技术,在有限变量逻辑中实现语法受限的公式与项精确学习、可实现性判定和合成。
本文研究有限变量逻辑中语法受限的公式与项精确学习问题:给定一组被正标记和负标记的有限结构,目标是学习一个公式或项,使其恰好分类这些结构。作者提出一种新颖且通用的自动机理论技术,将公式学习、可实现性判定与合成转化为自动机问题,并针对该问题给出算法以及复杂度上界和下界。该技术还被成功扩展至带最小不动点定义的一阶逻辑、高阶逻辑,以及查询与递归定义函数的项合成等变体。评估以理论结果为主,展示了方法在多种逻辑和学习问题上的适用性。
We consider grammar-restricted exact learning of formulas and terms in finite variable logics. We propose a novel and versatile automata-theoretic technique for solving such problems. We first show results for learning formulas that classify a set of positively- and negatively-labeled structures. We give algorithms for realizability and synthesis of such formulas along with upper and lower bounds. We also establish positive results using our technique for other logics and variants of the learning problem, including first-order logic with least fixed point definitions, higher-order logics, and synthesis of queries and terms with recursively-defined functions.