TY - GEN

T1 - Proving an Execution of an Algorithm Correct?

AU - Davenport, James Harold

PY - 2023/8/28

Y1 - 2023/8/28

N2 - 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”.

AB - 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”.

UR - http://www.scopus.com/inward/record.url?scp=85172096403&partnerID=8YFLogxK

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

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

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85172096403

SN - 9783031427527

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 255

EP - 269

BT - Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings

A2 - Dubois, Catherine

A2 - Kerber, Manfred

PB - Springer Science and Business Media Deutschland GmbH

CY - Cham, Switzerland

T2 - Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023

Y2 - 5 September 2023 through 8 September 2023

ER -