Computational logic and the social

Journal article

For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. ‘Crowdsourcing’ pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers, using programs designed to verify hardware, check proofs that are just too long and complicated for any human to comprehend. ‘Social machines’ are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. This paper outlines a research agenda for a new vision of a mathematics social machine, a combination of people, computers, and archives to create and apply mathematics, and places it in the context of verification research, computational logic and Roy Dyckhoff’s pioneering work on computer proof.

Authors: Martin, U

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Oxford University Press
• Journal: Journal of Logic and Computation
• Volume: 26
• Issue: 2
• Pages: 467-477
• Publication date: 2014-06-14
• DOI: 10.1093/logcom/exu036
• EISSN: 1465-363X
• ISSN: 0955-792X
• Keywords: proof systems; computational logic; logic teaching