Consequence Relations in Logics of AI

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.