Programowanie w logice 2006/2007

Pierwsza komputerówka, 14 listopada 2006

zadanie (pomysł E. Kopczyńskiego) | testy | moje rozwiązanie | rozwiązanie P. Mikulskiego | rozwiązanie P. Cerobskiego

Jak słusznie zauważył pan Cerobski, rozwiązanie pana Mikulskiego nie jest faktycznie liniowe. Dlaczego?

Pan Mikulski odpowiada, że konkurencyjne rozwiązanie również liniowe nie jest (kontrprzykład?) i proponuje poprawkę.

Bardzo zwięzłe i elegackie, choć nieoptymalne, rozwiązanie pana Macieja Kowalczyka.

Druga komputerówka, 12 grudnia 2006

zadanie | testy | moje rozwiązanie

Trzecia komputerówka, 23 stycznia 2007

zadanie | testy | moje rozwiązanie

Zadania zaliczeniowe

Jak pisać zadania zaliczeniowe?

Ciekawie! Tematy zadań powinny być możliwie nietrywialne i różnorodne. Programujcie Państwo to, co lubicie!
Efektywnie, czytelnie, elegancko! Program powinien być napisany i sformatowany przejrzyście. Należy stosować znaczące nazwy i wyczerpujące komentarze. Efektywność i elegancja rozwiązań będą oceniane.
Zrozumiale! Dokumentacja powinna zawierać dokładny opis zadania i rozwiązania. Należy zwrócić uwagę na ogólną ideę rozwiązania, rolę ważniejszych predykatów oraz precyzyjny opis i uzasadnienie poprawności nietrywialnych algorytmów.
Wygodnie, efektownie! Podręcznik użytkownika powinien zawierać dokładny opis funkcjonalności programu, instrukcje użycia programu, przykłady. Testy powinny prezentować ciekawe i imponujące przypadki.
Porządnie! Format: plik imie_nazwisko.gz, zawierający katalog imie_nazwisko z plikami program.pl, testy.pl, dokumentacja.tex, dokumentacja.pdf, podrecznik.tex, podrecznik.pdf (jak otworzę w Emacsie, to nie chcę mieć krzaków).
Szybko! Termin zatwierdzenia tematu: czwartek, 25 stycznia. Termin oddania zadań: poniedziałek, 5 lutego 2007.

Podział punktów

Funkcjonalność i zgodność z tematem - 25 pkt, dokumentacja - 10 pkt, podręcznik użytkownika - 5 pkt, testy - 10 pkt, efektywność - 10 pkt, elegancja i czytelność - 10 pkt.

Propozycje tematów

Tłumczenie formuł LTL na automaty alternujące.
Tłumczenie formuł MSO na automaty alternujące.
Tłumaczenie automatów alternujących na automaty deterministyczne.
Inkluzja języków rozpoznawanych przez automaty deterministyczne.
Tłumaczenie automatów ze stosem na DCG.

Zadania 1,3,4 mają stworzyć razem narzędzie do model-checkingu dla LTL, zadania 2,3,4 - dla MSO. Formuły LTL i MSO dostajemy w postaci napisów. Automat deterministyczny reprezentujemy jako term automat(listaPrzejsc, listaStanówPoczątkowych, listaStanowAkceptujacych), gdzie listaPrzejsc jest listą termów typu transition(stan, litera, stan). Automaty alternujące mają przejścia typu "jeśli jesteś w stanie p i widzisz literę a, to idź do q1 i q2 lub do r1, r2 i r3 lub do s1". Wygodnie będzie pamiętać taką tranzycję jako transition(q,a,[[q1,q2],[r1,r2,r3],[s1]]). Ogolnie, listaPrzejsc dla automatów alternujących jest listą termów typu transition(stan, litera, listaListStanow). Na liście przejść jest dokadnie jedno przejście dla każdej pary (stan, litera). W przypadku automatów alternujących, listaListStanow nie jest listą pustą i nie zawiera list pustych.

Filip Murlak 18-01-2007