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.