Czy istnieje rozsądny zautomatyzowany system dowodowy dla twierdzeń TCS?

28

Załóżmy, że chciałem sformalizować dowód Turinga dotyczący problemu zatrzymania, aby maszyna mogła to sprawdzić. Niektóre ze znanych automatycznych systemów dowodzenia twierdzeń obejmują Mizar, Coq i HOL4. Pobrałem i eksperymentowałem z Coq, ale nie ma biblioteki dla maszyn Turinga. Sam pomyślałem o kodowaniu jednego, ale brakowało tego samouczka, a język był trudny do odczytania.

Moje pytanie brzmi: czy istnieje automatyczna powiedzonka twierdzeń, która ogólnie dobrze sprawdza się w dowodzeniu twierdzeń dotyczących maszyn Turinga? Uznałbym, że taki twierdzący twierdzenie jest „dobry”, jeśli może sformalizować dowód nierozstrzygalności problemu zatrzymania przy użyciu już istniejących bibliotek. Uznałbym to za jeszcze lepsze, jeśli jest stosunkowo łatwo go podnieść. (Dla przypomnienia, zwykle nie mam trudności z językami programowania.)

Dzięki,

Philip

lo.logic turing-machines software proof-assistants automated-theorem-proving Philip White
źródło
Możesz sprawdzić tę stronę, ale lista nie zawiera problemu z zatrzymaniem.
Kaveh
10
Śmiem twierdzić, że musisz upierać się przy czymś takim jak Coq, zanim będzie to naturalne. I musisz być przy terminalu, pracując nad problemami, zamiast czytać książkę. Pomoże Ci zdobycie „Interaktywnego dowodzenia twierdzeń i opracowywania programu: Coq'Art: Rachunek konstrukcji indukcyjnych”. Poradniki Coq: cis.upenn.edu/~bcpierce/sf i adam.chlipala.net/cpdt są całkiem dobre (choć nie są skierowane bezpośrednio na to, czego chcesz).
Dave Clarke
5
Formalizacja dowodu może być dość skomplikowana, jeśli wybierzesz jego „złą” wersję. W przypadku problemu Halting sugerowałbym najpierw udowodnienie bardziej ogólnej i abstrakcyjnej wersji. Następnie możesz udowodnić później, że maszyny Turinga są specjalnym przypadkiem wersji abstrakcyjnej, jeśli nadal masz ochotę to zrobić (będzie bardzo wiele żmudnych szczegółów na temat maszyn Turinga, więc być może lepiej byłoby poświęcić czas na zrobienie czegoś innego). Pomyślę o dobrym sposobie udowodnienia tego w Coq. Bądź na bieżąco.
Andrej Bauer
5
Jeśli jesteś dobry w matematyce i w programowaniu, masz warunki wstępne, aby nauczyć się korzystać z asystenta dowodu. Naprawdę musisz traktować to jako nową umiejętność. (Jest to jednak bardzo satysfakcjonujące).
Neel Krishnaswami
Wygląda na to, że odpowiedź na pytanie brzmi „nie”. Myślę, że taki system byłby bardzo przydatny - czy mogę prosić o sformalizowanie maszyn Turinga, czy mógłbyś zastanowić się nad równoważnością czasu wielomianowego?
Colin McQuillan

Odpowiedzi:

17

Oto biblioteka Isabelle / HOL zawierająca twierdzenie Rice'a, które stwierdza nierozstrzygalność szerokiego zakresu problemów. Ponieważ ta biblioteka modeluje obliczalność za pomocą funkcji rekurencyjnych, musisz zakodować uniwersalną maszynę Turinga jako funkcję rekurencyjną, aby użyć tego twierdzenia do wykazania nierozstrzygalności problemu zatrzymania maszyn Turinga. Jednak zasadnicze części dowodu nierozstrzygalności zostały już wykonane.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
źródło