We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations.

翻译：我们提出了一种从示例中合成一阶逻辑公式的框架，该框架统一并推进了当前最先进的过渡系统不变式推理方法。为此，我们研究并分类了现有方法，通过答案集编程对其公式合成编码技术进行了分析。基于此分类，我们提出了正交切片——一种新的公式枚举技术，它将搜索空间划分为可管理的区块，从而实现了两种增量候选剪枝方法。通过结合现有的一阶不变式合成技术与我们在框架FORCE中实现的正交切片，我们显著加速了当前最先进的分布式系统不变式推理算法。我们还展示了我们的方法能够促进不同不变式推理框架的组合，从而实现新颖的优化。