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 | |
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 |
Funding
The author is supported by EPSRC grant EP/T015713. This paper was motivated by an invitation to speak at Machine-Assisted Proof, held at the Institute for Pure and Applied Mathematics at UCLA, and the author is very grateful to the Institute, the organisers, those who discussed the talk, and to Anne Baanen for some discussions. The author is grateful to Ali Uncu for his comments on several drafts.
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science