Knowledge-based programs

Peter Gammie 🌐

May 17, 2011


Knowledge-based programs (KBPs) are a formalism for directly relating agents' knowledge and behaviour. Here we present a general scheme for compiling KBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle's locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle's code generator.


BSD License


March 6, 2012
Add some more views and revive the code generation.


Session KBPs