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}