一千萬個為什麽

搜索

正式驗證的復雜性理論

是否有正在進行的項目使用像Coq這樣的證明助手來正式驗證復雜性理論的定理和證明?這樣做有什麽界限嗎?

最佳答案

In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)

轉載註明原文: 正式驗證的復雜性理論