|
|
|---|
|
|
|
|---|
A Linear Time Majority Vote Algorithm
In this book we prove the correctness of a linear time majority vote algorithm: given a list of elements determine which element occurs a majority of times in the list, assuming some such element occurs. The algorithm was invented by Bob Boyer and J Moore in 1980 and verified with their Nqthm theorem prover. However, the proof was not published until 1991. This proof is done in ACL2. For a detailed history of the algorithm, its proof, and its publication, see the long comment at the top of the majority-vote.lisp book.