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

这个项目将研究自动推理和逻辑 根据最近的一些发展，在多个编程- 有价值的注释逻辑。 这些逻辑被认为是 自动推理的统一形式化方法 系统通常必须执行推理任务， 经典逻辑不能自然地处理。 这些逻辑具有 被用作探索诸如推理等领域的工具。 不确定性，时间推理，以及推理 不一致的信息。 这项研究将检查自动演绎的框架 在注释逻辑中。 一个归结证明的适应性 程序将研究另一类多值 逻辑，调用Signed Formulas来执行自动推理， 注释逻辑 根据这项研究，一个统一的证明， 理论框架将发展为各种类 注释逻辑 效率和控制的问题 减少推理搜索空间的策略 规则将进行调查，并基于 理论成果将得到实施。

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.