合取查询、存在量词方程组与有限代换

本报告给出了正合取查询合一的基本理论。正合取查询是由命题常量、方程和原子通过使用合取 $\wedge$ 与存在量词 $\exists$ 构造的公式。特别地，空查询对应于存在量词方程组——称为 $\cal E$-公式。我们提供了一种将任意合取查询转化为求解形式的算法。我们证明了查询的一些格论性质。特别地，在等价关系下 $\cal E$-公式的商集构成一个完备格。随后我们给出另一个格——有限代换的格。我们证明这两个格同构。最后，我们引入代换对公式的作用的概念并阐明其与 $\cal E$-公式的关系。该理论可视为逻辑程序设计的另一种表述的基础。