Belief revision is a key functionality for any intelligent agent being able to perceive pieces of knowledge from its environment and to give back sentences she believes to be true with a certain degree of belief. We report on a refinement of a previous, abstract ASM specification of Condor, a system modeling such an agent, to a fully operational specification implemented in AsmL. The complete AsmL implementation of various belief revision operators is presented, demonstrating how using AsmL enabled a high-level implementation that minimizes the gap between the abstract specification of the underlying concepts and the executable code in the implemented system. Based on ASM refinement and verification concepts, a full mathematical correctness proof for different belief revision operators realized in Condor@AsmL is given.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{BeierleK08,
author = {Christoph Beierle and
Gabriele Kern{-}Isberner},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {A Verified AsmL Implementation of Belief Revision},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {98--111},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_9},
doi = {10.1007/978-3-540-87603-8\_9},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/BeierleK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}