Consequence Relations in Logics of AI

知识和关于知识的推理是人工智能和计算的基本概念。知识是数据，主要由事实组成。关于知识的推理涉及逻辑推理，即从已知事实推断出新知识的能力。对于各种形式的智力和论证概念的形式化来说，逻辑推理具有根本的重要性。逻辑推理在计算的几个领域也至关重要，从人工智能和软件工程到计算机语言和多智能体系统。一个正式指定的逻辑推论关系可以被描述为理论模型或理论证明（或两者都有）。逻辑结果可以表示为从一组句子到另一组句子的函数（塔斯基的首选表述），或者表示为两组句子之间的关系（多结论逻辑）。研究应用的逻辑推理不仅需要理解单一形式的逻辑推理。形式化逻辑结果的最常见方法包括公理和推理规则的选择。逻辑推理可以有多种选择，而选择的准确性会极大地影响逻辑推理的性质和效率。该项目的主要目的是寻找和开发人工智能和计算机科学逻辑中逻辑结果描述的技术。我们将特别关注模态逻辑中的逻辑结果，包括传统模态逻辑、时间逻辑和描述逻辑。模态逻辑在人工智能和计算机控制的基础和应用中起着特别重要的作用。由于图（Kripke/Hintikka结构）构成了模态型逻辑的语义基础，它们为通过图来研究计算的语义提供了很好的形式化方法，例如转换系统、解析树、Petri网、决策图和流程图。研究将解决的基本问题是：可以使用哪些推理规则，哪些推理规则是可接受的，有效的或可推导的，以及如何在实际和有效的证明系统中使用和实施它们。我们将研究和设计识别可接受推理规则的算法。另一个目的是研究可接受的和有效的推理规则的基础，找到基础的可能特征，确定有限基础可能的位置，从实现的角度构建有效的基础。推理规则的应用需要前提的统一性，因此我们计划研究逻辑统一性，并尝试构建检验统一性和构造统一性的算法。我们将从应用的角度研究领域逻辑的可接受推理规则的实现，以构建有效的证明系统。特别是，我们将研究和发展KE和模态型逻辑的自由变量表方法，实现开发的表决策程序并对其进行经验评估。

Knowledge and reasoning about knowledge are fundamental notions of AI and computation. The knowledge is data and consists primarily of facts. Reasoning about knowledge involves logical inference, i.e. the ability to infer new knowledge from known facts. For the formalisation of the notions of intelligence and argumentation in all forms, logical inference is of fundamental importance. Logical inference is also critically relevant in several areas of computing, ranging from AI and software engineering to computer languages and multi-agent systems. A formally specified logical consequence relation may be characterized model-theoretically or proof-theoretically (or both). Logical consequence can be expressed as a function from sets of sentences to sets of sentences (Tarski's preferred formulation), or as a relation between two sets of sentences (multiple-conclusion logic). The investigation of logical inference for applications requires not only the understanding of a single form of logical inference. The most common approach to formalise logical consequence consists of a choice of axioms and inference rules. Various choices are possible and the precise choice drastically influences the properties and efficiency of logical inference.The main aim of the project is, finding and developing of techniques for the description of logical consequence in logics of AI and CS. We will in particular focus on logical consequence in modal-type logics, including traditional modal logics, temporal logics, and description logics. Modal-type logics play an especially important role in the foundations and applications of AI and CS. Since graphs (Kripke/Hintikka structures) form the basis of the semantics for modal-type logics, they provide excellent formalisms for studying the semantics of computation via graphs, e.g. transition systems, parse trees, Petri nets, decision diagrams, and flow charts.Fundamental questions the research will address are: which inference rules may be used, which inference rules are admissible, valid or derivable and how they may be used and implemented in practical and efficient proof systems. We will study and devise algorithms recognising admissible inference rules. Another aim is to investigate bases for admissible and valid inference rules, to find possible characterisations for bases, determine where finite bases are possible, to construct bases effective from the viewpoint of implementations. Applications of inference rules require unification of the premises, therefore we plan study of logical unification and attempt to construct algorithms for checking unifiability and constructing unifiers. We will investigate implementations of admissible inference rules for the logics of the domain area from viewpoint of applications to construct effective proof systems. In particular, we will study and develop KE and free-variable tableau approaches for modal-type logics, implement the developed tableau decision procedures and evaluate them empirically.