A Cooperative Grid Computing Approach to Automated Theorem Finding and Automated Problem Proposing

摘要

This paper proposes a novel research direction: to build the Theory Grid as cooperatively shared formal theories within a virtual organization, and then to implement a crowd of automated reasoning programs working based on the Theory Grid such that as the wisdom of crowds a grid theorist has the ability to find new theorems and propose new questions automatically or semi-automatically. The paper also presents an architecture of the Theory Grid and grid theorists, and major scientific challenges and technical issues in the implementation of the Theory Grid and grid theorists.