This paper presents the development of a software tool that enables the translation of first-order predicate logic with at most three variables into relation algebra. The tool was developed using the Z3 theorem prover, leveraging its capabilities to enhance reliability, generate code, and expedite development. The resulting standalone Python program allows users to translate first-order logic formulas into relation algebra, eliminating the need to work with relation algebra explicitly. This paper outlines the theoretical background of first-order logic, relation algebra, and the translation process. It also describes the implementation details, including validation of the software tool using Z3 for testing correctness. By demonstrating the feasibility of utilizing first-order logic as an alternative language for expressing relation algebra, this tool paves the way for integrating first-order logic into tools traditionally relying on relation algebra as input.

翻译：本文介绍了一种软件工具的开发，该工具能够将最多包含三个变量的一阶谓词逻辑公式转换为关系代数。该工具利用Z3定理证明器构建，充分发挥其增强可靠性、生成代码和加速开发的能力。最终形成的独立Python程序允许用户将一阶逻辑公式转换为关系代数，从而无需直接处理关系代数。本文阐述了一阶逻辑、关系代数及转换过程的理论基础，同时详细描述了实现细节，包括使用Z3验证软件工具的正确性。通过证明利用一阶逻辑作为表达关系代数的替代语言的可行性，该工具为将一阶逻辑集成到传统上依赖关系代数作为输入的工具中铺平了道路。