Основной источник эквивалентности недетерминированного полиномиального времени и детерминированной полиномиальной проверки времени

Кто первым показал, что язык находится в NP, если сертификат для языка можно проверить за полиномиальное время? У нас есть документ, который формально доказывает это? Когда сообщество TCS начало преуменьшать недетерминизм в пользу проверяемости? Для жизни я не могу найти хорошую ссылку на это помимо текстов, таких как Пападимитриу, Арора и Барак.

[Расширенный комментарий] Я думаю, что «корни проверки» уже содержатся в веховом докладе Карпа «Сократимость среди комбинаторных проблем» (1972):

...
Пусть обозначает класс подмножеств , распознаваемых за полиномиальное время. Для и полинома мы определим следующим образом:$P^{(2)}$$\Sigma^* \times \Sigma^*$$L^{(2)} \in P^{(2)}$$p$$L$

$L = \{ x \mid$ существует st и$y$$\langle x,y \rangle \in L^{(2)}$$\log(y) \leq p(\log(x)) \}$

(однако Карп не вызывает «Свидетельство»)$y$

... Мы называем языком, полученным из помощью ограниченной экзистенциальной квантификации.$L$$L^{(2)}$$p$

Определение 4 . - это множество языков, полученных из элементов путем ограниченного полиномами экзистенциального квантования.$NP$$P^{(2)}$

Существует альтернативная характеристика NP с точки зрения недетерминированных машин Тьюринга ... [определение вычисления недетерминированной машины Тьюринга] ...

и

... Теорема 1 : тогда и только тогда, когда принимается недетерминированной машиной Тьюринга, работающей за полиномиальное время ...$L \in NP$$L$