Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems

逻辑推理和自动推理方法是Web技术和Agent技术在大型本体的智能处理、基于结构化数据知识库的决策以及多Agent系统的形式化规范和验证等方面的关键技术，目前用于本体推理的表描述逻辑推理机存在一些明显的不足。这些问题包括表达能力不足、复杂性欠佳、过于专业化和不完整的正式处理。所有这些都是严重的问题，需要解决和克服，如果这样的系统是形成骨干本体推理的语义Web。关于多智能体系统内的推理和关于多智能体系统的推理，以智能体的智能决策和智能体系统的形式规范和验证的形式，存在着大量的智能体逻辑已经提出了用于此目的，但几乎没有实现的推理系统，解决这些逻辑中的可满足性和有效性问题。这种缺乏系统支持是一个严重的问题。我们将使用一阶逻辑和决议的技术来开发一个决议框架推理表达本体语言和表达代理逻辑。将开发一系列工具，为这些领域的推理任务提供自动化支持。将研究、设计基准原则，并将其用于对已开发技术和工具的实证调查。

Logical and automated reasoning methods are crucial for web technologies and agent technologies for the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems.Concerning ontology reasoning the current tableau description logic reasoners used for this purpose have a number of significant shortcomings. These include insufficient expressiveness, suboptimal complexity, over specialisation and incomplete formal treatment. All these are serious issues which need to be tackled and overcome if such systems are to form the backbone ontology reasoning for the semantic web. Concerning reasoning within and about multi-agent systems, in the form of intelligent decision making by agent and the formal specification and verification of agent systems, there exists a plethora of agent logics which have been proposed for this purpose, but almost no implemented reasoning systems for solving satisfiability and validity problems in these logics. This lack of system support is a serious problem.We will use techniques from first-order logic and resolution to develop a resolution framework for reasoning about expressive ontological languages and expressive agent logics. A series of tools will be developed to provide automated support for reasoning tasks in these areas. Principles of benchmarking will be studied, designed and used for empirical investigations of developed technologies and tools.