将一阶谓词逻辑翻译成关系代数，使用Z3实现
摘要：用Z3定理证明器开发了一款软件工具，可以将一阶谓词逻辑翻译成关系代数。该工具利用了Z3的能力，提高了可靠性、生成代码并加快了开发过程。结果是一个独立的Python程序，允许用户将一阶逻辑表达式转化为关系代数，无需直接使用关系代数。本论文概述了一阶逻辑、关系代数和翻译过程的理论背景，还描述了实现细节，包括使用Z3进行正确性测试的工具验证，并讨论了与原始翻译过程的偏差。通过展示利用一阶逻辑作为表达关系代数的替代语言的可行性，该工具为将一阶逻辑整合到传统上依赖关系代数作为输入语言的工具中铺平了道路。
作者：Anthony Brogni, Sebastiaan J. C. Joosten
论文ID：2308.02513
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-08