一阶环和环公式在非经典逻辑计算中的理论与应用

知识的表示和推理是人工智能研究的核心内容之一，非单调逻辑是描述人类表示现实世界知识和推理的重要工具。非单调逻辑研究的一个共同的问题是实现和计算比较困难，这极大的限制了它的应用。另一方面，经典的一阶谓词逻辑是人们研究的最为彻底的逻辑系统，同时经典逻辑的证明系统和模型求解系统的理论研究和系统实现非常成熟。.在[LZ2004]中定义的环和环公式为基于答集的逻辑程序和经典逻辑的转化提供了一个有力的工具，[CLWZ2006]将这一结果推广到了一阶的情况，并且表明它可以适用于更广泛的非单调逻辑的领域。我们希望以此为基础在一阶环和环公式理论的指导下，实现一个一阶的回答集求解器，并且进一步研究非单调逻辑和经典逻辑的关系，将其中一些结果推广到其它非单调逻辑，以实现利用现有经典逻辑求解器的非单调逻辑计算。