No Cover Image

Conference Paper/Proceeding/Abstract 214 views 21 downloads

Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda

Harry Bryant, Andrew Lawrence, Monika Seisenberger Orcid Logo, Anton Setzer Orcid Logo

Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea, Pages: 1 - 5

Swansea University Authors: Harry Bryant, Monika Seisenberger Orcid Logo, Anton Setzer Orcid Logo

DOI (Published version): 10.5281/ZENODO.17946910

Published in: Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea
Published: Zenodo 2025
Online Access: https://doi.org/10.5281/zenodo.17946910
URI: https://cronfa.swan.ac.uk/Record/cronfa71159
first_indexed 2025-12-18T20:27:17Z
last_indexed 2026-01-23T06:52:01Z
id cronfa71159
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2026-01-22T12:44:39.7231530</datestamp><bib-version>v2</bib-version><id>71159</id><entry>2025-12-18</entry><title>Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda</title><swanseaauthors><author><sid>2efb4f6a3eec27ae4337ecd971aaeca4</sid><firstname>Harry</firstname><surname>Bryant</surname><name>Harry Bryant</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-12-18</date><deptcode>MACS</deptcode><abstract/><type>Conference Paper/Proceeding/Abstract</type><journal>Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea</journal><volume/><journalNumber/><paginationStart>1</paginationStart><paginationEnd>5</paginationEnd><publisher>Zenodo</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>18</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-12-18</publishedDate><doi>10.5281/ZENODO.17946910</doi><url>https://doi.org/10.5281/zenodo.17946910</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2026-01-22T12:44:39.7231530</lastEdited><Created>2025-12-18T20:10:37.5002328</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Harry</firstname><surname>Bryant</surname><order>1</order></author><author><firstname>Andrew</firstname><surname>Lawrence</surname><order>2</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>3</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>4</order></author></authors><documents><document><filename>71159__35861__fe9f661f41614d22955ee0ed1e295df6.pdf</filename><originalFilename>ccc2025_bryant-setzer-lawrence-seisenberger.pdf</originalFilename><uploaded>2025-12-18T20:25:20.1050773</uploaded><type>Output</type><contentLength>515996</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2026-01-22T12:44:39.7231530 v2 71159 2025-12-18 Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda 2efb4f6a3eec27ae4337ecd971aaeca4 Harry Bryant Harry Bryant true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2025-12-18 MACS Conference Paper/Proceeding/Abstract Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea 1 5 Zenodo 18 12 2025 2025-12-18 10.5281/ZENODO.17946910 https://doi.org/10.5281/zenodo.17946910 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2026-01-22T12:44:39.7231530 2025-12-18T20:10:37.5002328 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Harry Bryant 1 Andrew Lawrence 2 Monika Seisenberger 0000-0002-2226-386X 3 Anton Setzer 0000-0001-5322-6060 4 71159__35861__fe9f661f41614d22955ee0ed1e295df6.pdf ccc2025_bryant-setzer-lawrence-seisenberger.pdf 2025-12-18T20:25:20.1050773 Output 515996 application/pdf Accepted Manuscript true false
title Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
spellingShingle Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
Harry Bryant
Monika Seisenberger
Anton Setzer
title_short Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
title_full Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
title_fullStr Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
title_full_unstemmed Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
title_sort Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda
author_id_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4
d035399b2b324a63fe472ce0344653e0
5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4_***_Harry Bryant
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Harry Bryant
Monika Seisenberger
Anton Setzer
author2 Harry Bryant
Andrew Lawrence
Monika Seisenberger
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea
container_start_page 1
publishDate 2025
institution Swansea University
doi_str_mv 10.5281/ZENODO.17946910
publisher Zenodo
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url https://doi.org/10.5281/zenodo.17946910
document_store_str 1
active_str 0
published_date 2025-12-18T05:34:35Z
_version_ 1856987071443369984
score 11.096212

Similar Items