Abstract
Incompleteness and undecidability have been used for many years as arguments against automatising the practice ofmathematics. 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.
Cite
CITATION STYLE
Calude, C. S., & Thompson, D. (2016). Incompleteness, undecidability and automated proofs (Invited talk). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9890 LNCS, pp. 134–155). Springer Verlag. https://doi.org/10.1007/978-3-319-45641-6_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
