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.