| Powrót do listy seminariów |
| 2006-05-23, godz. 16:00-18:00, s. 5850 |
| Lidia Stępień i Marian Srebrny (Akademia Jana Dlugosza, Czestochowa i IPI PAN) |
| Propositional Calculus as a Programming Environment for Linear Algebra |
| In this talk we will present an application of a propositional satisfiability, SAT, solving environment to certain computational tasks in the area of the algebraic theory of quadratic forms; more precisely, in the theory of Witt rings of quadratic forms. As known in algebra, the problem of finding homomorphisms of an elementary Witt ring can be reduced to searching for some special kind of bases of certain vector space over the two-element Galois field. We show how this can be coded as a propositional formula in such a way that its satisfying valuations code the desired bases. Having got all the bases of the considered space one can determine all the automorphisms of the corresponding ring. Some encouraging experimental results will be given for the proposed search procedure using the currently best SAT solvers. |
| 2006-05-09, godz. 16:00-18:00, s. 5850 |
| dr KONRAD ZDANOWSKI (Uniwersytet Warszawski Wydzial Filozofii) |
| Interpretacja arytmetyki z ograniczona indukcja w arytmetyce Robinsona |
| Przedstawimy definiowalny odcinek poczatkowy
modeli dla arytmetyki Robinsona, ktory spelnia
indukcje dla formul z kwantyfikacja ograniczona.
Omowiona konstrukcja odkryta zostala przez Solovay'a.
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2006-04-25, godz. 16:00-18:00, s. 5850 |
| dr KONRAD ZDANOWSKI (Wydzial Filozofii UW) (Uniwersytet Warszawski) |
| "Interpretacja arytmetyki $I\Delta_0$ w arytmetyce Robinsona" |
| Oto autorskie streszczenie:
Przedstawimy, pochodzaca od Solovaya,
metode interpretacji arytmetyki $I\Delta_0$
w arytmetyce Robinsona. Zostala ona ostanio
wykorzystana przez Svejdera dla pokazania
istotnej nierozstrzygalnosci pewnego oslabienia
arytmetyki Robinsona zdefiniowanego przez Grzegorczyka.
Zapraszamy serdecznie wszystkich zainteresowanych!
A.Grzegorczyk
A.Salwicki
M.Srebrny Więcej informacji: http://www.mimuw.edu.pl/~salwicki?PPIM |
| 2006-03-28, godz. 16:00-18:00, s. 5850 |
| prof. Andrzej Grzegorczyk (IFIS PAN, d. IM UW, d. IMPAN) |
| Wszystko co wiadomo i czego nie wiadomo o teorii Konkatenacji, a co jest ciekawe do zrobienia |
| Podsumowanie wyników uzyskanych przez prelegenta w dziedzinie teorii konkatenacji. Przypomnijmy: uzyskano m.in. wynik o nierozstrzygalności tej teorii analoiczny do tw. Goedla, ale bez "arytmetyzacji", wprost.
Omówione też zostana problemy otwarte.
Podczas seminarium prelegent udostępni odbitki swej najnowszej pracy. Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/28marz2006.pdf |
| 2005-05-31, godz. 16:15-18:00, s. 5870 |
| Maciej Szreter (Instytut Podstaw Informatyki PAN) |
| Efektywne testowanie spelnialnosci formul zdaniowych |
| Testowanie spelnialnosci formul zdaniowych (SAT) jest czesto
analizowane dla formul generowanych losowo oraz dla formul kodujacych
pewne problemy. W przypadku tej drugiej klasy wykorzystanie informacji
o strukturze problemu moze umozliwic istotne zwiekszenie efektywnosci
algorytmu. W referacie zostanie zaprezentowane takie rozwiazanie dla
Ograniczonej Weryfikacji Modelowej (Bounded Model Checking, BMC).
Istota BMC jest zakodowanie problemu weryfikacji modelowej poprawnosci
programow jako formuly zdaniowej, przy czym wartosciowanie spelniajace
dostarcza kontrprzyklad. Pokazemy, jak przy testowaniu takich formul
zastosowac w standardowym algorytmie SAT-DPLL redukcje
czesciowo-porzadkowe, popularna optymalizacje stosowana w weryfikacji
nie-symbolicznej.
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/ |
| 2005-05-09, godz. 16:15-18:00, s. 5870 |
| Michal Matusiak (Uniwersytet Warszawski) |
| Propositional satisfiability - a new version of the DPLL algorithm. |
| Abstract
A new version, called mmSAT, of the Davis-Putnam-Logemann-Loveland algorithm will be presented. It has recently been proposed in my MSc thesis, together with implementation. The experimental results obtained are encouraging: on over 30 benchmark formulas it scores
better than zChaff, currently most respected SAT solver. Although, we are worse on over 100 other benchmarks. The algorithm mmSAT is an extension of DPLL by some new mechanisms of drawing conclusions from 2-clauses, conflict analysis and learning. Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/ |
| 2005-04-05, godz. 16:10-18:00, s. 5870 |
| Seminarium odwołane i przesunięte na 12 kwietnia br. |
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/ |
| 2005-03-15, godz. 16:10-17:40, s. 5870 |
| Andrzej Salwicki (Instytut Informatyki Uniwersytet Warszawski) |
| Dlaczego pewien program zapętla się |
| Na przykładzie pewnego prostego programu chcemy:
1. przedstawić kilka niemal banalnych obserwacji o związku instrukcji iteracji z kwantyfikatorami, o numerowaniu krotek, ...
2. zbudować formułę stopu tego programu i udowodnić ją,
3. zachęcić do poszukiwania nowego dowodu.
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/ |
| 2005-03-01, godz. 16:10-17:40, s. 5870 |
| Jerzy Mycka (Uniwersytet Marii Curie-Skłodowskiej) |
| "Obliczalność analogowa - niestandardowe metody dla klasycznych problemów obliczalności" |
| W referacie zostaną krótko zaprezentowane podstawowe modele obliczeń
analogowych - GPAC Shannona, EAC Rubela, R-rekurencyjne funkcje Moore'a.
W celu rozwiązania problemów związanych z powyższymi modelami zostanie
zaproponowana definicja rzeczywistych funkcji rekurencyjnych.
Określone zostaną podstawowe własności modelu oraz oparta
na nim \eta-hierarchia. Następnie wskazane zostaną związki rzeczywistych
funkcji rekurencyjnych z klasyczną obliczalnością (symulacja maszyn Turinga,
relacja do hierarchii arytmetycznej i hierarchii Grzegorczyka)
oraz klasami Baire'a i obliczalnością na liczbach rzeczywistych
w sensie Mazura. Jako istotny wynik zostaną pokazane definicje podklas
rzeczywistych funkcji rekurencyjnych AnalogP i AnalogNP oraz ich związki
z klasami złożoności P i NP. Przedyskutowane zostaną wewnętrzne
ograniczenia modelu (problemy nierozstrzygalne względem rzeczywistych funkcji
rekurencyjnych) oraz związki z proponowanymi teoriami obliczeń silniejszych
niż maszyny Turinga (superobliczalność).
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2005-02-22, godz. 16:10-17:40, s. 5870 |
| M. Kurkowski (Akademia Jana Dugosza Częstochowa) |
| A propositional knowledge logic of authentication |
| We interpret authentication protocols (programs) in the set of all the
possible computations. Each computation is modelled as a sequence of
states generated by performing the basic actions of the program, one at
a time. Concurrent activity of two parallel sessions is represented by
the interleaving of the interpretations of the atomic actions.
The basic Boolean valued atomic predicates expressing a participant's
knowledge sets, and some relations of interest for authentication, are
incorporated into the framework of classical propositional logic.
A complete axiomatization will be presented. A proof of the
completeness
theorem will be given. An algorithm of deciding tautologies will be
shown.
Więcej informacji: http://www.mimuw.edu.pl/~salwicki?PPIM |
| 2005-01-11, godz. 16:10-18:00, s. 5870 |
| M. Kurkowski (WSP Częstochowa) |
| Verification of cryptographic protocols |
| One of the crucial issues in open distributed computer network is communications security, which is usually achieved by applying specially designed distributed programs called security protocols. Practice shows that there is a need to specify these protocols in some formalism and to verify their correctness. In the recent several years a lot of attention has been paid to this problem and a few methods have been introduced to investigate it. One of the ways is to construct deduction systems expressive enough to allow description of the protocol and its correctness property. Burrows, Abadi, Needham and others have proposed a few logics for verification of the authentication protocols. These are some versions of modal logic with special constructs for expressing some of the central concepts used in authentication processes. In this talk the main emphasis will be on the knowledge of protocols users (agents, participants, players). We will introduce a new mechanically decidable complete knowledge-authentication logic convenient for specifying and reasoning about properties of the authentication protocols. We provide an axiomatic inference system, a computation structure, and semantics. We show completeness, decidability and some other important properties of this logic. We also present and discuss its expressive power, for example the protocol correctness property. We believe that this semantics is good enough for the model checking techniques, to verify the authentication protocols widely used in today's practice. |
| 2004-12-14, godz. 16:10-18:00, s. 5870 |
| Konrad Zdanowski (Instytut Matematyczny PAN) |
| Finite Arithmetic - coprimality |
| Główny wynik, który będzie przedstawiony podczas tego odczytu to twierdzenie, że w rodzinie skończonych arytmetyk z relacją względnej perwszości można zdefiniować i dodawanie i mnożenie.
Zobacz abstrakt odczytu na stronie seminarium! Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-11-30, godz. 16:15-18:00, s. 5870 |
| Konrad Zdanowski (IM PAN) |
| Finite Arithmetics |
| Let FM(A), for A = (\omega; : : :), be a family of finite, initial segments of A.
One can see FM(A) as a family of finite arithmetics related to the arithmetic
A.
In the talk I will survey what is known about such arithmetics and their
logical properties. The main questions will be the following: What is the complexity
of theories of such families? What relations can be represented in such
families? What are the possible ways to represent some infinite relations? What
are the definabilities between such arithmetics?
Especially, we focus our attention on finite arithmetics of the form:
FM((\omega;+;£)), FM((\omega;*)), FM((\omega;?)), where +, *, ? are addition, multiplication
and coprimality relation, respectively. Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-11-16, godz. 16:10-18:00, s. 5870 |
| prof. Andrzej Grzegorczyk, Andrzej Salwicki (Uniwersytet Warszawski) |
| Omówienie nowych i starych zadań. Planowanie referatów |
| Z pewnym opóźnieniem(przepraszamy)seminarium PPIM rozpoczyna prace.
Podczas pierwszego w tym semestrze spotkania omówione zostaną stare i nowe zadania i problemy.
Ustalimy plan referatów. Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-05-18, godz. 16:10-18:00, s. 5790 |
| dr Andrzej Zbrzezny (Wydzial Matematyki i Informatyki WSP czestochowa) |
| Zastosowanie SAT do testowania osiagalnosci dla automatow czasowych |
| Jednym z aspektow weryfikacji poprawnosci systemow tranzycyjnych jest
testowanie wlasnosci bezpieczenstwa. Mowimy, ze system jest
P-bezpieczny, jezeli nie jest w nim osiagalny zaden stan spelniajacy
wlasnosc P.
W referacie zostanie przedstawiona korzystajaca z SAT metoda testowania
osiagalnosci dla sieci komunikujacych sie automatow czasowych, ktore
stosowane sa do modelowania systemow czasu rzeczywistego. Istota tej
metody polega na skonstruowaniu formuly R(k,P) stwierdzajacej istnienie
w modelu wykonan weryfikowanego systemu sciezki o dlugosci k, na ktorej
osiagalny jest stan majacy niepozadana wlasnosc P. Nastepnie formula
R(k,P) poddawana jest translacji do formuly zdaniowej Q w taki sposob,
ze prawdziwosc formuly R(k,P) jest rownowazna zdaniowej spelnialnosci
formuly Q.
Zarysowana metoda szczegolnie dobrze nadaje sie do testowania
osiagalnosci, a w konsekwencji do stwierdzenia faktu, iz weryfikowany
system nie jest poprawny. Niemniej, jak zostanie pokazane, pewne
rozszerzenie tej metody, pozwala niekiedy na testowanie nieosiagalnosci,
a tym samym na stwierdzenie, iz weryfikowany system jest poprawny ze
wzgledu na zadana wlasnosc.
Praktyczna stosowalnosc prezentowanej metody zostanie zilustrowana
wynikami eksperymentalnymi dla sparametryzowanego czasem protokolu
wzajemnego wykluczania. Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-05-11, godz. 16:10-18:00, s. 5790 |
| dr Maciej Szreter (IPI PAN) |
| Algorytmy testowania spełnialności formul rachunku zdan (SAT) |
| W referacie zostanie przedstawiony przeglad stanu wiedzy w dziedzinie
automatycznego testowania spelnialnosci formul rachunku zdan (SAT).
Intensywne badania w tej dziedzinie zostaly rozpoczete w drugiej polowie
XX wieku i doprowadzily do opracowania wielu interesujacych rozwiazan.
Jest to jeden z przykladów udanej realizacji maszynowego dowodzenia dla
pewnego fragmentu logiki. Realizacji praktycznie efektywnej na wielu
interesujacych formulach, mimo wykladniczej w najgorszym przypadku zlozonosci znanych obecnie testerow SAT.
W ostatnich latach algorytmy SAT osiagnely wysoki poziom zaawansowania
i zaczely byc stosowane do rozwiazywania problemow z innych dziedzin
matematyki i informatyki.
Opisowi algorytmow beda towarzyszyc demonstracje programow, w ktorych
je zaimplementowano.
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-04-20, godz. 16:10-18:00, s. 5790 |
| Mateusz Srebrny (Uniwersytet Warszawski) |
| Factorization with SAT - classical propositional calculus as programming environment |
| Propositional satisfiability, SAT, is one of the best known NP-complete problems. There is no feasible algorithm known for testing satisfiability of propositional formulas in general. Nevertheless, there are algorithms (implemented by so called SAT solvers or SAT checkers)that turn out surprisingly efficient (feasible) for many instances of
propositional formulas.
On the other hand, for the problem of integer factorisation no one knows any polynomial time solving algorithm. A famous and challenging cryptosystem RSA was built on it in 1977 and has been widely applied since then.
In this talk, a polynomial time translation of integer factorisation into propositional formulas, along with some hopefully interesting experimental results with currently best SAT solvers will be presented and discussed.
Notes to this talk will be available from Monday
from www.mimuw.edu.pl/~salwicki/PPIM
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-04-06, godz. 16:15-18:00, s. 5790 |
| Andrzej Salwicki (Instytut Informatyki, Uniwersytet Warszawski) |
| Czy elementarna teoria kolejek jest rozstrzygalna? |
| Struktury danych: kolejki i kolejki dwustronne sa znane i powszechnie stosowane. Na pytanie czy ich specyfikacja w jezyku logiki pierwszego rzędu jest rozstrzygalna nie znamy dotąd odpowiedzi. Więcej informacji: http://duch.mimuw.edu.pl/~salwicki/PPIM/ElemQueues.pdf |
| 2004-03-30, godz. 16:10-18:00, s. 5790 |
| prof. A. Grzegorczyk (IFIS PAN) |
| O istotnej nierozstrzygalności teorii konkatenacji |
| Nowy wynik Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-03-23, godz. 16:15-18:00, s. 5790 |
| Konrad Zdanowski (Instytut Filozofii) (Uniwersytet Warszawski) |
| Interpretacje mnożenia w modelu standardowym konkatenacji |
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-03-16, godz. 16:15, s. 5790 |
| posiedzenie odwołane - z powodu choroby |
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM |
| 2004-03-09, godz. 16:15-18:00, s. 5790 |
| Konrad Zdanowski (Instytut Filozofii UW) (Uniwersytet Warszawski) |
| Definiwalność mnożenia w standardowym modelu konkatenacji |
| 2004-02-17, godz. 16:15-18:00, s. 5790 |
| prof. Andrzej Grzegorczyk (Uniwersytet Warszawski) |
| Dowód nierozstrzygalności matematyki bez użycia arytmetyzacji |
Więcej informacji: http://www.mimuw.edu.pl/~salwicki/PPIM/ref1Grzeg.html |