Knowledge-based programs

Peter Gammie 🌐

May 17, 2011

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

License

BSD License

History

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

Topics

Session KBPs

Depends on

Used by

Cite

× 
@article{KBPs-AFP,
  author  = {Peter Gammie},
  title   = {Knowledge-based programs},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2011},
  note    = {\url{https://isa-afp.org/entries/KBPs.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: