Proving an Execution of an Algorithm Correct?

James Harold Davenport

doi:10.1007/978-3-031-42753-4_17

Proving an Execution of an Algorithm Correct?

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

1 Citation (SciVal)

Abstract

Many algorithms in computer algebra and beyond produce answers. For some of these, we have formal proofs of the correctness of the algorithm, and for others it is easy to verify that the answer is correct. Other algorithms produce either an answer or a proof that no such answer exists. It may still be easy to verify that the answer is correct, but what about the “no such answer” case. The claim of this paper is that, at least in some cases, it is possible for the algorithm to produce “hints” such that a theorem prover can prove that, in this case, there is no such answer. This leads to the paradigm of “ad hoc UNSAT verification”.

Original language	English
Title of host publication	Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings
Editors	Catherine Dubois, Manfred Kerber
Place of Publication	Cham, Switzerland
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	255-269
Number of pages	15
ISBN (Electronic)	9783031427534
ISBN (Print)	9783031427527
DOIs	https://doi.org/10.1007/978-3-031-42753-4_17
Publication status	Published - 28 Aug 2023
Event	Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023 - Cambridge, UK United Kingdom Duration: 5 Sept 2023 → 8 Sept 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14101 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023
Country/Territory	UK United Kingdom
City	Cambridge
Period	5/09/23 → 8/09/23

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-42753-4_17

Cite this

Davenport, J. H. (2023). Proving an Execution of an Algorithm Correct? In C. Dubois, & M. Kerber (Eds.), Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings (pp. 255-269). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14101 LNAI). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-42753-4_17

Proving an Execution of an Algorithm Correct? / Davenport, James Harold.
Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings. ed. / Catherine Dubois; Manfred Kerber. Cham, Switzerland: Springer Science and Business Media Deutschland GmbH, 2023. p. 255-269 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14101 LNAI).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Davenport, JH 2023, Proving an Execution of an Algorithm Correct? in C Dubois & M Kerber (eds), Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14101 LNAI, Springer Science and Business Media Deutschland GmbH, Cham, Switzerland, pp. 255-269, Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023, Cambridge, UK United Kingdom, 5/09/23. https://doi.org/10.1007/978-3-031-42753-4_17

Davenport JH. Proving an Execution of an Algorithm Correct? In Dubois C, Kerber M, editors, Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings. Cham, Switzerland: Springer Science and Business Media Deutschland GmbH. 2023. p. 255-269. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2023 Aug 1. doi: 10.1007/978-3-031-42753-4_17

Davenport, James Harold. / Proving an Execution of an Algorithm Correct?. Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings. editor / Catherine Dubois ; Manfred Kerber. Cham, Switzerland : Springer Science and Business Media Deutschland GmbH, 2023. pp. 255-269 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b7ae6678f0e740bcb4e1d38d901216e7,

title = "Proving an Execution of an Algorithm Correct?",

abstract = "Many algorithms in computer algebra and beyond produce answers. For some of these, we have formal proofs of the correctness of the algorithm, and for others it is easy to verify that the answer is correct. Other algorithms produce either an answer or a proof that no such answer exists. It may still be easy to verify that the answer is correct, but what about the “no such answer” case. The claim of this paper is that, at least in some cases, it is possible for the algorithm to produce “hints” such that a theorem prover can prove that, in this case, there is no such answer. This leads to the paradigm of “ad hoc UNSAT verification”.",

author = "Davenport, {James Harold}",

year = "2023",

month = aug,

day = "28",

doi = "10.1007/978-3-031-42753-4_17",

language = "English",

isbn = "9783031427527",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "255--269",

editor = "Catherine Dubois and Manfred Kerber",

booktitle = "Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings",

address = "Germany",

note = "Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023 ; Conference date: 05-09-2023 Through 08-09-2023",