Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems

对于大型本体的智能处理、基于结构化数据知识库的决策以及多智能体系统的形式化描述和验证，逻辑推理和自动推理方法是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.