30.10.2003

Formalizmy logiczne a programowanie deklaratywne

W referacie tym dyskutujemy dwa formalizmy wywodzące się z logiki matematycznej: spelnialność i programowanie logiczne z semantyka modeli stabilnych. Oba te formalizmy pozwalają na rozwiazywanie takich problemów przeszukiwania które znajdują się w klasie zwanej NP-search. Wiele problemów kombinatorycznej optymalizacji takie jak znajdowanie cyklu Hamiltona, kolorowania grafów i podobne znajdują się w tej klasie. W ostatnich latach osiagnięto znaczny postęp w dziedzinie systemów implementujących każdy z tych formalizmów. Systemy takie nazywane są często "solverami". Skomentujemy stan badań w dziedzinie zupełnych i probabilistycznych solverów. Przedstawimy zagadnienia związane ze zbudowaniem jezyków które mogą służyć do programowania nad tymi systemami. Na koniec przedstawimy szereg wyników uzyskanych poprzez zastosowanie owych solverów do klasycznych problemów kombinatorycznych. W szczególności pokazemy pewna ilość nowych ograniczeń dolnych na klasyczne liczby van der Waerdena dotyczace istnienia ciagów arytmetycznych w blokach podziałów.