#### Majority Vote Algorithm Revisited Again

In his article \*Experience with Software Specification and
Verification Using LP, the Larch Proof Assistant*, Manfred Broy verified
(as one of his smaller case studies) the Majority Vote Algorithm by Boyer and
Moore. LP requires that all user theories are expressed axiomatically. I
reworked the example in Isabelle/HOL and turned it into a definitional
development, thus proving its consistency. In the end, a short alternative
proof is given.
pdf
IJSI version

BibTeX:

@article{Nipkow-IJSI11,author={Tobias Nipkow},
title={Majority Vote Algorithm Revisited Again},
journal={International Journal of Software and Informatics},
volume=5,pages={21-28},year=2011}