经典逻辑和描述逻辑中的可满足性问题

逻辑公式的可满足性问题是计算机科学和人工智能中的重要问题之一。本项目将结合若干应用领域中的具体问题来研究各种形式的可满足性判定问题。这些应用领域包括：语义Web，硬件设计，有限数学等等。要研究的问题主要是：经典的命题逻辑、一阶谓词逻辑以及描述逻辑中各种公式的模型构造，逻辑与数值混合公式的可满足性判定。本项目的主要研究目标是为这些问题寻找高效率的算法，并实现相应的原型工具。具体地说，要解决的关键问题包括：一阶逻辑公式有限模型搜索过程中的搜索策略；一阶逻辑公式有限模型构造器和SAT求解器的结合；命题公式和数值约束相混合的可满足性判定问题；RDF图之间蕴含关系的判断；与OWL语言相关的推理问题，比如一致性检查。