Algorithm for Modal-Clause Resolution to Support Epistemic Reasoning in Multi-Agent Systems
Abstract
The ability to reason about other agents' beliefs has many applications in multi-agent systems, including facilitating coordinated behavior, teamwork, and information exchange. Modal logics are commonly used to formally capture and reason about knowledge/belief states. Unlike in propositional logic, it is computationally complex to create an automatic deduction algorithm capable of proving entailment when modal operators are considered. In this paper, we present an extension of a propositional logic resolution theorem prover to resolve modal clauses based on a complete set of inference rules for KD that was previously published by Enjalbert and del Cerro in 1989. We demonstrate that this modal resolution theorem prover, EpiRes, can be used for epistemic belief reasoning in an Information Privacy application domain by showing what an observer can infer by monitoring the actions of another agent. In this setting, a robot inspects nuclear reactor facilities for high or low radiation levels in varying locations depending on the reactor type. The goal of the observer is to try to infer the reactor type by monitoring the actions of the robot, which requires reasoning about the robot’s goals, information obtained by actions, and justifying why the robot took the actions it took. To more easily model this scenario, we created a modal, meta operator “knows whether” (KW) for writing rules that are agnostic to the true state of the world and provide the equivalent translation in KD. We conclude by showing that EpiRes was successful in showing what information can or cannot be inferred by the observer from different actions (plans) of the robot, without having to model belief states explicitly as sets of possible worlds.
Citation
Mrosko, Bryson Kyle (2023). Algorithm for Modal-Clause Resolution to Support Epistemic Reasoning in Multi-Agent Systems. Undergraduate Research Scholars Program. Available electronically from https : / /hdl .handle .net /1969 .1 /200287.