Meaning-preserving Skolemization
Meaning-preserving Skolemization
复制标题
保留意义的斯科莱姆化
DOI：
10.5220/0003692003220327
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Ekawit Nantajeewarawat
中科院分区：
文献类型：
--
作者：
K. Akama;Ekawit Nantajeewarawat
斯科勒姆化是一种著名的从逻辑公式中删除存在量词的方法。虽然它总是产生一个保持可满足性的变换步骤，但经典斯科勒姆化通常不保留源公式的逻辑意义。本文发展了一种通过合并函数变量来扩展逻辑公式空间的理论，并展示了如何在所获得的扩展空间中实现保义Skolem化。描述了将逻辑公式转换为扩展空间上扩展合取范式的等价公式的过程。该工作为基于保义公式变换的存在量词逻辑问题的求解奠定了理论基础。
Skolemization is a well-known method for removing existential quantifiers from a logical formula. Although it always yields a satisfiability-preserving transformation step, classical Skolemization in general does not preserve the logical meaning of a source formula. We develop in this paper a theory for extending a space of logical formulas by incorporation of function variables and show how meaning-preserving Skolemization can be achieved in an obtained extended space. A procedure for converting a logical formula into an equivalent one in an extended conjunctive normal form on the extended space is described. This work lays a theoretical foundation for solving logical problems involving existential quantifications based on meaning-preserving formula transformation.