Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Knowledge-Based Programs

Email Gateway (Aug 18 2022 at 17:43):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
We're pleased to announce the availability of a new AFP entry on [http://afp.sf.net] that accompanies the ITP'11 paper of the same title:

Title: Knowledge-based programs
Author: Peter Gammie

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.

Cheers,
Gerwin

Last updated: Nov 21 2024 at 12:39 UTC