Gödel's Poetry

Kelly J. Davis

Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. We introduce here a new approach to computer theorem proving, one that employs spe…