Agents' Logics with Common Knowledge and Uncertainty: Unification Problem, Algorithm for Construction Solutions

摘要

This paper studies agents' logics with operation uncertainty. Prime attention is paid to agents' common knowledge logics with logical operation uncertainty and logical unification in these logics. The unification problem is: for two arbitrary given formulas with meta-variables (coefficients) to answer whether they are unifiable, and if yes to construct a unifier. This problem is equivalent to problem of solvability logical equations with coefficients and finding theirs solutions. We show that the basic common knowledge logic with uncertainty operation (notation - CKL_(n,U)) is decidable w.r.t. logical unification of the common knowledge formulas, and that for unifiable common knowledge formulas we can construct a unifier (we may describe solving algorithm). This result is extended to a wide class of logics expanding CKL_(n,U).