文件列表:

Cardinality.v (2833, 2016-01-30)
Elementary.v (21846, 2016-01-30)
LICENSE (1059, 2016-01-30)
Makefile (734, 2016-01-30)
Scales.v (84615, 2016-01-30)

Scales A classic puzzle involves determining the minimum number of times a scale must be used to find a single fake coin in a collection of coins. This project concerns using formal methods to prove properties regarding such puzzles. In particular, we prove that the algorithm given for finding a fake coin known to be lighter than the real coins is optimal for any number of coins. This proof is formalized in Coq. Enjoy, Fred Smith

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：