Email Gateway (Oct 22 2021 at 08:58): Email Gateway (Oct 22 2021 at 08:58):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
I'm happy to announce a new AFP entry by Valentin Fouillard, Safouan Taha, Frédéric
Boulanger and Nicolas Sabouret: Belief Revision Theory
Abstract:
The 1985 paper by Carlos Alchourrón, Peter Gärdenfors, and David Makinson (AGM), “On the
Logic of Theory Change: Partial Meet Contraction and Revision Functions” launches a large
and rapidly growing literature that employs formal models and logics to handle changing
beliefs of a rational agent and to take into account new piece of information observed by
this agent. In 2011, a review book titled "AGM 25 Years: Twenty-Five Years of Research in
Belief Change" was edited to summarize the first twenty five years of works based on AGM.
This HOL-based AFP entry is a faithful formalization of the AGM operators (e.g.
contraction, revision, remainder ...) axiomatized in the original paper. It also contains
the proofs of all the theorems stated in the paper that show how these operators combine.
Both proofs of Harper and Levi identities are established.
You find it online at https://www.isa-afp.org/entries/Belief_Revision.html
With this entry, we've reached 400 authors who have contributed to the AFP!
Enjoy,
Andreas
Last updated: Jul 15 2022 at 23:21 UTC