Abstract

VSK logic is a family multi-modal logics for reasoning about the information properties of computational agents situated in some environment. Using VSK logic, we can represent what is objectively true of the environment, the information that is visible, or knowable about the environment, information the agent perceives of the environment, and finally, information the agent actually knows about the environment. The semantics of VSK logic are given in terms of a general, automata-like model of agents. In this paper, we prove completeness for an axiomatisation of VSK logic, and present correspondence results for a number of VSK interaction axioms in terms of the architectural properties of the agent that they represent. The completeness proof is novel in that we are able to prove completeness with respect to the automata-like semantics. In this sense, VSK logic is said to be computationally grounded. We give an example to illustrate the formalism, and present conclusions and issues for further work