Uncomputable games: games for crowdsourcing formal reasoning.

摘要

This work presents two games, the Catabot Rescue Game (CRG) and the Catabot Building Game (CBG), that capture theorem proving in first-order logic. The scope of the thesis is to invent and design the first games which both capture theorem proving in first- order logic and can also be played by players without having any knowledge of formal logic. The thesis successfully launches a project, "The Uncomputable Games Project," that seeks to use game playing by crowds for use in theorem proving. Many important science, engineering, and computational problems require at least first-order logic to be formalized. (Note: All computational problems can be cast in first-order logic.) Since first- order theorem proving is Turing-undecidable, no amount of algorithmic development or hardware improvement will ever be enough to help us realistically tackle all the problems we might be interested in. The games presented here could eventually help us harvest creative, general-purpose problem-solving at a massive scale. An abstract and simple for- malization of the proof construction workspace Slate is used as a background to show that the games capture first-order theorem proving. While implementing the full versions of the games and demonstrating new theorems being proved in first-order logic is beyond the scope of the thesis, initial data from early implementations for propositional logic is presented. While we do not have experiments for the full first-order case, some promise can be seen in that users untrained in logic were able to find proofs in propositional logic shorter than those found by an automated theorem prover.