RUI: A Framework for Automated Deduction Systems in MultipleValued Annotated Logics

这个项目将基于多值注释逻辑的一些最新发展来研究自动演绎和逻辑编程。这些逻辑被提倡作为自动推理系统的统一形式化的一种方式，这些自动推理系统经常必须执行经典逻辑不能自然处理的推理任务。这些逻辑已被用作探索不确定推理、时间推理以及不一致信息推理等领域的工具。这项研究将检验《注释逻辑》中自动演绎的框架。对于另一类多值逻辑，调用符号公式来执行注释逻辑中的自动推理，将研究归结证明过程的适应性。在此研究的基础上，将为各种类型的注释逻辑建立一个统一的证明理论框架。研究了减少推理规则搜索空间的效率和控制策略问题，并实现了一个基于理论结果的原型系统。

This project will investigate automated deduction and logic programming based on some recent developments in Multiple- Valued Annotated Logics. These logics have been advocated as a way to a uniform formalization of automated reasoning systems that often have to perform reasoning tasks which classical logics cannot handle naturally. These logics have been used as tools to explore areas such as reasoning with uncertainty, temporal reasoning, as well as reasoning with inconsistent information. This research will examine frameworks for automated deduction in Annotated Logics. The adaptation of a resolution proof procedure will be studied for another class of Multiple-Valued Logics, call Signed Formulas to perform automated reasoning in Annotated Logics. Based on this study, a unifying proof theoretic framework will be developed for the various classes of Annotated Logics. The question of efficiency and control strategies for reducing the search space of the inference rules will be investigated, and a prototype system based on the theoretical results will be implemented.