Research On Intuitionistic Epistemic Logic

Epistemic logic is a subfield of model logic that is concerned with knowledge reasoning and belief change.Epistemic logic is widely used in Artificial intelligence,multi-agent systems and Game Theory.For a long time,the academia has carried out a deep and extensive study of epistemic logic on the basis of classical logic,and established corresponding logic system to depict different types of knowledge.In recent years,a group of scholars have combined intuitionistic and epistemic logic to study epistemic logic on the basis of intuitionistic logic.This study provides a new logical tool for the research in the field of computer science that emphasizes tectonics and flexibility.As we all know,intuitionistic logic is based on the BHK(Brouwer-Heyting-Kolmogrov)semantics of the proof concept,the algebraic semantics based on Heyting algebra,and the Kripke semantics based on truth.Kripke structure is one of the important semantic structures of modal logic.It is easy to understand and similar to many structures in formal methods.The logical language in this structure can be used as a specification language to describe the nature of computing system.Therefore,many studies on intuitionist epistemic logic are based on the Kripke structure.However,due to the semantic interpretation of epistemic modal words and intuitionistic negatives,the reachability relations of these Kripke structures need more constraints.This makes it difficult to construct models in the completeness of related logic systems.Especially for logic systems containing modality such as common knowledge with the semantic characteristics of fixed point,the usual canonical model method is not effective in many cases.The paper aims at exploring epistemic logic deal with common knowledge and distributed knowledge in intuitionistic logic.Main work includes:1.Base on intuitionistic epistemic logic ICK,establishes its completeness and soundness of the axiom system IDS4 which deals with the intuitionistic distributed knowledge with positive introspection by model transformation,unifies the proof of IDK,IDT and IDS4's completeness and soundness.2.Deal with distributed knowledge and common knowledge in intuitionistic logic at the same time,provides axiom systems ICDK,ICDT which deal with the intuitionistic distributed knowledge and common knowledge for differernt reachable relation,establishes its completeness and soundness.