Incompleteness, Undecidability and Automated Proofs

Calude, CS; Thompson, D

dc.contributor.author	Calude, CS	en
dc.contributor.author	Thompson, D	en
dc.date.accessioned	2017-02-07T03:37:17Z	en
dc.date.available	2017-02-07T03:37:17Z	en
dc.date.issued	2016	en
dc.identifier.citation	CDMTCS Research Reports CDMTCS-497 (2016)	en
dc.identifier.issn	1178-3540	en
dc.identifier.uri	http://hdl.handle.net/2292/31754	en
dc.description.abstract	Incompleteness and undecidability have been used for many years as arguments against automatising the practice of mathematics. The advent of powerful computers and proof-assistants – programs that assist the development of formal proofs by human-machine collaboration – has revived the interest in formal proofs and diminished considerably the value of these arguments. In this paper we discuss some challenges proof-assistants face in handling undecidable problems – the very results cited above – using for illustrations the generic proof-assistant Isabelle.	en
dc.publisher	Department of Computer Science, The University of Auckland, New Zealand	en
dc.relation.ispartofseries	CDMTCS Research Report Series	en
dc.rights	Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated. Previously published items are made available in accordance with the copyright policy of the publisher.	en
dc.rights.uri	https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm	en
dc.source.uri	https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/index.php	en
dc.title	Incompleteness, Undecidability and Automated Proofs	en
dc.type	Technical Report	en
dc.subject.marsden	Fields of Research	en
dc.rights.holder	The author(s)	en
dc.rights.accessrights	http://purl.org/eprint/accessRights/OpenAccess	en