Thông tin tài liệu


Nhan đề : Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
Tác giả : Yong Kiam, Tan
Marijn J. H., Heule
Magnus O., Myreen
Năm xuất bản : 2023
Nhà xuất bản : Springer
Tóm tắt : 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.
Mô tả: CC BY
URI: https://link.springer.com/article/10.1007/s10009-022-00690-y
https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368
Bộ sưu tậpOER - Công nghệ thông tin
XEM MÔ TẢ

23

XEM TOÀN VĂN

20

Danh sách tệp tin đính kèm: