Andrzej M. BorzyszkowskiAndrzej M.
	Borzyszkowski
Logika – laboratorium (JAPE)

Dedukcja naturalna

Jest to zestaw reguł służący do dowodzenia twierdzeń w rachunku zdań oraz rachunku predykatów pierwszego rzędu. Reguły naturalnej dedukcji dla rachunku zdań zostały przedstawione na wykładzie 1, ich zestaw znajduje się tutaj. Laboratoria w tej części poświęcone będą prowadzeniu dowodów za pomocą reguł naturalnej dedukcji ze wspomaganiem systemu JAPE.

Edytor dowodów JAPE

Został napisany przez Bernarda Sufrina i Richarda Bornata z Uniwersytetu w Oksfordzie. Pozwala nie tylko prowadzić wnioskowania metodą dedukcji naturalnej dla rachunku zdań i rachunku predykatów, ale oferuje również wspomaganie dowodzenia w innych logikach, a także pozwala definiować własne systemy dedukcyjne (wymaga to oczywiście dodatkowej wiedzy :). W przypadku metody dedukcji naturalnej w wariancie intuicjonistycznym JAPE wspomaga również proces znajdywania kontrprzykładów metodą „wymuszania” (forsingu).

Instalacja JAPE'a pod Linuksem

Interfejs użytkownika JAPE napisany został w języku Java i do działania wymaga jedynie obecności maszyny wirtualnej JVM. Instalacja programu jest banalnie prosta.

Uwaga! Proszę użyć przygotowanego archiwum, a nie pakietu dystrybucyjnego dla Linuksa z witryny JAPE'a.

Instalacja JAPE-a pod Windows

Aby zainstalować JAPE-a pod Windows należy zacząć od pobrania pakietu instalacyjnego. Po jego uruchomieniu należy wybrać docelowy katalog instalacji. Najlepiej, aby ścieżka do niego była w miarę krótka (załóżmy, że będzie to „x:\katalog\Jape”). Po wybraniu katalogu docelowego, zaznaczamy jeszcze opcję „Shortcut on Desktop” i naciskamy guzik Install, a potem Exit...

Po zakończeniu instalacji, pobieramy i zapisujemy do katalogu „x:\katalog\Jape\examples\natural_deduction” następujące pliki:

W przypadku drugiego pliku zastępujemy istniejącą już w katalogu docelowym inną jego wersję. Na zakończenie musimy jeszcze zmodyfikować właściwości skrótu służącego do uruchamiania JAPE-a. W tym celu do wartości pola „Element docelowy” dodajemy odstęp, a po nim „x:\katalog\Jape\examples\natural_deduction\I2L.jt”. Naciskamy Zastosuj i OK. JAPE jest już poprawnie zainstalowany pod Windows.

Praca z JAPE

Po wczytaniu pliku z sekwentami do udowodnienia pojawia się jeden lub więcej paneli z zadaniami. Nas będzie interesować opcja "prove" dla każdego wskazanego sekwentu. Po wybraniu tej opcji pojawia się okienko z przesłankami na górze (o ile są obecne) z wnioskiem na dole i wielokropkiem w środku. Należy doprowadzić do usunięcia wielokropka poprzez stosowanie reguł naturalnej dedukcji. Jest kilka możliwości

Dowody poszczególnych sekwentów można zachować na bieżąco w momencie zamykania okienka z dowodem. Można zapisać bieżący stan pracy (ale nie dowód pojedynczego sekwenty, jedynie wszystkich już udowodnionych). Można też wygenerować plik postscriptowy dla pojedynczego dowodu i wydrukować taki dowód.

Uwaga 2. JAPE nie oferuje jako „podstawowej” reguły eliminacji podwójnej negacji ¬¬e. Zamiast niej daje nam do dyspozycji regułę klasycznego dowodu nie wprost, w jego nomenklaturze: contra (classical)

¬φ
––––(nie wprost)
φ

Reguła ¬¬e jest konsekwencją zastosowania reguły contra (classical) oraz reguły eliminacji negacji ¬e. Z drugiej strony, reguła dowodu nie wprost wynika z ¬¬e i pozostałych reguł rachunku zdań. Jeszcze jedną różnicą w stosunku do zestawu reguł wprowadzonego na wykładzie jest fakt, że regułę eliminacji sprzeczności ⊥e JAPE nazywa regułą „konstruktywnego dowodu nie wprost” – contra (constructive).

Dokumentacja JAPE

Natural Deduction Proof and Disproof in Jape.

Do góry