一句话：提出 Folloy，将一阶逻辑规约学习编码为 Alloy 中的约束满足问题，并用 Max-SAT 保证所学公式规模最小。
一阶逻辑（FOL）适合刻画系统不变式与性质，但其形式化复杂度阻碍了实际采用。本文提出 Folloy，一个从示例中合成一阶逻辑规约的工具。其核心贡献是把规约学习转化为约束满足问题：在 Alloy Analyzer 中以声明式方式建模 FOL 的语法与语义，因此方法具有较强表达力，可合成非前束范式（non-prenex）公式，并支持用户自定义的语法约束。借助 Max-SAT 求解器，Folloy 还能保证所学公式在规模上最小。作者在基准问题上进行评估，结果显示：该通用方法虽比专用算法慢，但能求解更广的一类问题，从而在性能与表达力之间形成权衡。
First-Order Logic (FOL) is a powerful language for specifying system invariants and properties, yet its formal complexity often hinders its adoption. To address this, we present Folloy, a tool that synthesizes FOL specifications from examples. Our core contribution translates specification learning into a constraint satisfaction problem by declaratively modeling FOL syntax and semantics in the Alloy Analyzer. This method is expressive, allowing synthesis of non-prenex formulas and user-defined syntactic constraints. By leveraging a Max-SAT solver, Folloy also guarantees that the learned formula is minimal in size. We evaluate our tool on benchmark problems and show that while this general approach is slower than a specialized algorithm, it solves a broader class of problems, establishing a trade-off between performance and expressive power.
DOI 原文 ·
@inproceedings{paperbot9400,
title = {First-Order Quantified Separator in Alloy Analyzer},
author = {One An},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00391}
}