|
||||||||||||||||
|
Ph.D. ThesesUncomputable Games: Games for Crowdsourcing Formal Reasoning
By Naveen Sundar Govindarajulu
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-uncomputable, 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 formalization of the proof construction workspace Slate is used as a background to show that the games capture first-order theorem proving. Initial data from early implementations is presented. Early promising results show that even users untrained in logic can find proofs in propositional logic shorter than those found by an automated theorem prover.
|
||||||||||||||||
Research
