形式的に検証された複雑さの理論

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.)

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です