Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Abstrakt

Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs.

In this paper, we describe a formalized theory of size-optimal sorting networks. From this formalization we extract a certified checker that successfully verifies computer-generated proofs of optimality on up to 8 inputs. The checker relies on an untrusted oracle to shortcut the search for witnesses on more than 1.6 million NP-complete subproblems.
OriginalsprogEngelsk
TitelInteractive Theorem Proving : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
RedaktørerChristian Urban, Xingyuan Zhang
ForlagSpringer
Publikationsdato2015
Sider154-169
ISBN (Trykt)978-3-319-22101-4
ISBN (Elektronisk)978-3-319-22102-1
DOI
StatusUdgivet - 2015
NavnLecture Notes in Computer Science
Vol/bind9236
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker'. Sammen danner de et unikt fingeraftryk.

Citationsformater