Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
CC BY
Lưu vào:
| Tác giả chính: | , , |
|---|---|
| Định dạng: | Sách |
| Ngôn ngữ: | English |
| Nhà xuất bản: |
Springer
2023
|
| Chủ đề: | |
| Truy cập trực tuyến: | https://link.springer.com/article/10.1007/s10009-022-00690-y https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368 |
| Từ khóa: |
Thêm từ khóa
Không có từ khóa, Hãy là người đầu tiên đánh dấu biểu ghi này!
|
| id |
oai:localhost:PNK-7368 |
|---|---|
| record_format |
dspace |
| spelling |
oai:localhost:PNK-73682023-03-31T03:11:45Z Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML Yong Kiam, Tan Marijn J. H., Heule Magnus O., Myreen SAT LPR CC BY Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy (PR ). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This article describes the first approach to formally verify PR proofs on a succinct representation. We present (i) a new Linear PR (LPR) proof format, (ii) an extension of the DPR-trim tool to efficiently convert PR proofs into LPR format, and (iii) cake_lpr, a verified LPR proof checker developed in CakeML. 2023-03-31T03:11:45Z 2023-03-31T03:11:45Z 2023 Book https://link.springer.com/article/10.1007/s10009-022-00690-y https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368 en application/pdf Springer |
| institution |
Digital Phenikaa |
| collection |
Digital Phenikaa |
| language |
English |
| topic |
SAT LPR |
| spellingShingle |
SAT LPR Yong Kiam, Tan Marijn J. H., Heule Magnus O., Myreen Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| description |
CC BY |
| format |
Book |
| author |
Yong Kiam, Tan Marijn J. H., Heule Magnus O., Myreen |
| author_facet |
Yong Kiam, Tan Marijn J. H., Heule Magnus O., Myreen |
| author_sort |
Yong Kiam, Tan |
| title |
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| title_short |
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| title_full |
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| title_fullStr |
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| title_full_unstemmed |
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML |
| title_sort |
verified propagation redundancy and compositional unsat checking in cakeml |
| publisher |
Springer |
| publishDate |
2023 |
| url |
https://link.springer.com/article/10.1007/s10009-022-00690-y https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368 |
| _version_ |
1761912524871041024 |
| score |
8.887836 |