ウィリアム・マキューン

ウィリアム・ウォーカー・マキューン（1953年12月17日 - 2011年5月2日）は、自動推論、代数学、論理学、形式手法の分野で活躍したアメリカのコンピュータ科学者および論理学者である。

彼は、 Otter、Prover9、Mace4といった自動推論システムの開発、およびEQP定理証明器を用いたロビンス予想の自動証明で最もよく知られている。

2000年、マッキューンは自動推論への顕著な貢献に対してハーブランド賞を受賞した。^{[ 1 ]} 2013年には、彼を称えて『自動推論と数学 ― ウィリアム・W・マッキューン追悼論文集』が出版された。^{[ 2 ]}

• Prover9ソフトウェア
• ウィリアム・マキューンのホームページ
• Prover9ソフトウェアのアップデート版