一句话：提出用逻辑学习与合成技术自动发现结构类的公理化，并在部分情形自动证明完备性。
公理与推理规则是演绎系统的基础，但传统上发现公理化往往依赖专家的大量手工工作。本文探索能否用合成技术自动为一类类结构发现公理化，并在某些语境下自动证明其完备性。方法上，作者将逻辑学习与合成结合，系统性地搜索并构造适合目标结构类的公理和推理规则。评估涵盖两个场景：一是模态逻辑中可由一阶逻辑刻画的框架类，二是带有正则运算的语言模型类。结果表明，合成技术能够为这些结构类发现公理，并在部分情形下自动获得完备性证明，展示了自动发现公理化的可行性。
Axioms and inference rules form the foundation of deductive systems and are crucial in the study of reasoning with logics over structures. Historically, axiomatizations have been discovered manually with much expertise and effort. In this paper we show the feasibility of using synthesis techniques to discover axiomatizations for different classes of structures, and in some contexts, automatically prove their completeness. For evaluation, we apply our technique to find axioms for (1) classes of frames in modal logic characterized in first-order logic and (2) the class of language models with regular operations.
@article{paperbot1442,
title = {Synthesizing axiomatizations using logic learning},
author = {Paul Krogmeier and Zhengyao Lin and Adithya Murali and P. Madhusudan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563348}
}