What can be learned from failed proofs of non-theorems?
This paper reports an investigation into the link between failed proofs and non-theorems. It seeks to answer the question of whether anything more can be learned from a failed proof attempt than can be discovered from a counter-example. We suggest that the branch of the proof in which failure occu...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Oxford University Computing Laboratory
2005
|
| Online Access: | https://eprints.nottingham.ac.uk/297/ |
| _version_ | 1848790389117419520 |
|---|---|
| author | Dennis, Louise Abigail Nogueira, Pablo |
| author2 | Hurd, Joe |
| author_facet | Hurd, Joe Dennis, Louise Abigail Nogueira, Pablo |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | This paper reports an investigation into the link between failed proofs and non-theorems. It seeks to answer the question of whether anything more can be learned from a failed proof attempt than can be discovered from a counter-example. We suggest that the branch of the proof in which failure occurs can be mapped back to the segments of code that are the culprit, helping to locate the error.
This process of tracing provides finer grained isolation of the offending code fragments than is possible from the inspection of counter-examples. We also discuss ideas for how such a process could be automated. |
| first_indexed | 2025-11-14T18:11:50Z |
| format | Conference or Workshop Item |
| id | nottingham-297 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:50Z |
| publishDate | 2005 |
| publisher | Oxford University Computing Laboratory |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-2972020-05-04T20:30:46Z https://eprints.nottingham.ac.uk/297/ What can be learned from failed proofs of non-theorems? Dennis, Louise Abigail Nogueira, Pablo This paper reports an investigation into the link between failed proofs and non-theorems. It seeks to answer the question of whether anything more can be learned from a failed proof attempt than can be discovered from a counter-example. We suggest that the branch of the proof in which failure occurs can be mapped back to the segments of code that are the culprit, helping to locate the error. This process of tracing provides finer grained isolation of the offending code fragments than is possible from the inspection of counter-examples. We also discuss ideas for how such a process could be automated. Oxford University Computing Laboratory Hurd, Joe Smith, Edward Darbari, Ashish 2005 Conference or Workshop Item NonPeerReviewed Dennis, Louise Abigail and Nogueira, Pablo (2005) What can be learned from failed proofs of non-theorems? In: Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, September, Oxford. |
| spellingShingle | Dennis, Louise Abigail Nogueira, Pablo What can be learned from failed proofs of non-theorems? |
| title | What can be learned from failed proofs of non-theorems? |
| title_full | What can be learned from failed proofs of non-theorems? |
| title_fullStr | What can be learned from failed proofs of non-theorems? |
| title_full_unstemmed | What can be learned from failed proofs of non-theorems? |
| title_short | What can be learned from failed proofs of non-theorems? |
| title_sort | what can be learned from failed proofs of non-theorems? |
| url | https://eprints.nottingham.ac.uk/297/ |