Czy jest jakiś realizowany projekt formalnej weryfikacji twierdzeń i dowodów teorii złożoności przy użyciu asystenta dowodu, takiego jak Coq? Czy są jakieś granice?
3
Myślę, że niektóre badania są prowadzone na uniwersytecie w Bolonii przy pomocy asystenta Matity. Zobacz na przykład Formalizowanie maszyn Turinga .
—
Marzio De Biasi
Powiązane: cstheory.stackexchange.com/q/4052/129 . Niektóre odpowiedzi mówią nawet o Coq, a inne wspominają o wynikach, które można interpretować jako teoretyczne bariery dla tego projektu, choć prawdopodobnie nie są to bariery w praktyce.
—
Joshua Grochow
Dzięki, to pytanie było świetne @JoshuaGrochow, więc cieszę się, że dowiedziałem się o monografii Hartmannisa. Jeśli rozumiem, barierą byłoby upewnienie się, że zdefiniowane przez ciebie klasy złożoności są tym, co według nich są, a nie wersją „możliwą do udowodnienia w Coq”.
—
Samuel Schlesinger
To prawda, ale to istotne. Zastanawiam się, w jaki sposób pomocny system typów mógłby pomóc, na przykład poprzez włączenie pewnych pojęć złożoności do typów funkcji. Oczywiście doprowadziłoby to do szerokiego zakresu równości, ale myślę, że i tak mamy naturalnie złożoność.
—
Samuel Schlesinger