Przeskocz do treści

Delta mi!

Loading

Twierdzenie o niepustym barze, czyli zmechanizowana naturalna dedukcja

Jacek Chrząszcz

o artykule ...

  • Publikacja w Delcie: kwiecień 2017
  • Publikacja elektroniczna: 30 marca 2017
  • Wersja do druku [application/pdf]: (82 KB)

Sprawdzanie poprawności dowodów matematycznych często wymaga sporej wiedzy i ogromu nużącej pracy. O ile dochodzenie do zrozumienia istoty dowodu, czyli dlaczego dane twierdzenie matematyczne zachodzi, może sprawiać Czytelnikowi dużo satysfakcji, o tyle weryfikowanie wszystkich szczegółów dowodu jest zajęciem dość niewdzięcznym. Z tego powodu od wielu już lat trwają badania nad zaprzęgnięciem komputerów do tej żmudnej części pracy...

obrazek

Sprawdzanie poprawności dowodów matematycznych często wymaga sporej wiedzy i ogromu nużącej pracy. O ile dochodzenie do zrozumienia istoty dowodu, czyli dlaczego dane twierdzenie matematyczne zachodzi, może sprawiać Czytelnikowi dużo satysfakcji, o tyle weryfikowanie wszystkich szczegółów dowodu jest zajęciem dość niewdzięcznym. Z tego powodu od wielu już lat trwają badania nad zaprzęgnięciem komputerów do tej żmudnej części pracy...

Aktualnie nie istnieją programy, które potrafią rozumieć dowody matematyczne napisane po polsku lub po angielsku (i ogólnie, w żadnym języku naturalnym). Istnieją za to systemy z własnym językiem opisu dowodu, mniej lub bardziej oddalonym od języka naturalnego. Jednym z takich systemów jest Coq, rozwijany głównie we Francji, w instytucie naukowym INRIA. Jest to interaktywny system pozwalający na poszukiwanie dowodów twierdzeń za pomocą zwięzłych komend, nazywanych taktykami.

Każda taktyka odpowiada z grubsza zastosowaniu pewnej reguły dowodzenia zwanej naturalną dedukcją. Coq nie służy do automatycznego dowodzenia twierdzeń, do działania potrzebuje ludzkich podpowiedzi. Każdą podpowiedzianą taktykę stosuje bezbłędnie, uzyskując wszystkie możliwe wnioski i sprawdzając, co jeszcze należy udowodnić, żeby dowód analizowanego twierdzenia był kompletny. W niniejszym artykule zaprezentujemy dowód w Coqu, wykonany z użyciem reguł naturalnej dedukcji, następującego twierdzenia:

Twierdzenie. W każdym niepustym barze jest taka osoba, że jeśli ona pije, to wszyscy piją.

Choć twierdzenie brzmi absurdalnie, jednak da się je udowodnić. Przyczyny tego dysonansu omówimy później, a teraz rozważmy dwa dowody.

  • Cały artykuł dostępny jest w wersji do druku [application/pdf]: (82 KB)

Coq można pobrać ze strony coq.inria.fr (wersja wymagająca instalacji). Eksperymentalna wersja on-line jest dostępna na stronie x80.org/collacoq/. Po załadowaniu (co może potrwać nawet minutę) w prawym dolnym rogu (Packages) należy kliknąć w chmurkę coq-base, powodując załadowanie odpowiedniego pakietu. Następnie do lewego panelu można wpisać treść dowodu w Coqu i poruszać się po nim, używając strzałek w prawym panelu.