On using Theorem Proving for Cognitive Agent-oriented Programming

Demonstrating reliability of cognitive multi-agent systems is of key importance. There has been an extensive amount of work on logics for verifying cognitive agents but it has remained mostly theoretical. Cognitive agent-oriented programming languages provide the tools for compact representation of complex decision making mechanisms, which offers an opportunity for applying a theorem proving approach. We base our work on the belief that theorem proving can add to the currently available approaches for providing assurance for cognitive multi-agent systems. However, a practical approach using theorem proving is missing. We explore the use of proof assistants to make verifying cognitive multi-agent systems more practical.