Projekty finansowane przez NCN


Dane kierownika projektu i jednostki realizującej

Szczegółowe informacje o projekcie i konkursie

Słowa kluczowe

Aparatura

Wyczyść formularz

Procedury decyzyjne w weryfikacji

2011/03/B/ST6/00346

Słowa kluczowe:

problem decyzyjny weryfikacja logika automatyczne dowodzenie twierdzeń

Deskryptory:

  • ST6_7: Teoretyczne podstawy informatyki, w tym informatyka kwantowa
  • ST1_1: Logika i podstawy matematyki

Panel:

ST6 - Informatyka i technologie informacyjne: technologie i systemy informacyjne, informatyka, obliczenia naukowe, systemy inteligentne

Jednostka realizująca:

Uniwersytet Wrocławski, Wydział Matematyki i Informatyki

woj. dolnośląskie

Inne projekty tej jednostki 

Kierownik projektu (z jednostki realizującej):

prof. Witold Charatonik 

Liczba wykonawców projektu: 5

Konkurs: OPUS 2 - ogłoszony 2011-09-15

Przyznana kwota: 483 450 PLN

Rozpoczęcie projektu: 2012-08-31

Zakończenie projektu: 2016-02-29

Planowany czas trwania projektu: 42 miesięcy (z wniosku)

Status projektu: Projekt rozliczony

Zakupiona aparatura

  1. Komputer przenośny. Za kwotę 10 000 PLN
  2. Komputer z wydajnym procesorem i dużą pamięcią operacyjną. Za kwotę 10 000 PLN

Dane z raportu końcowego/rocznego

  • Publikacje w czasopismach (6)
  • Teksty w publikacjach pokonferencyjnych (5)
  1. Bounded Model Checking of Pointer Programs Revisited
    Autorzy:
    Witold Charatonik, Piotr Witkowski
    Czasopismo:
    The Computing Research Repository (CoRR) (rok: 2016, tom: abs/1602.09061, strony: 45315), Wydawca: arXiv.org
    Status:
    Opublikowana
  2. Complexity of Two-Variable Logic on Finite Trees
    Autorzy:
    Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, James Worrell
    Czasopismo:
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC (rok: 2016, tom: 17(4), strony: 32:1 - 32:38), Wydawca: ACM
    Status:
    Opublikowana
    Doi:
    10.1145/2996796 - link do publikacji
  3. Parameterized complexity of basic decision problems for tree automata
    Autorzy:
    Witold Charatonik and Agata Chorowska
    Czasopismo:
    International Journal of Computer Mathematics (rok: 2013, tom: 90(6), strony: 1150-1170), Wydawca: Taylor & Francis
    Status:
    Opublikowana
    Doi:
    10.1080/00207160.2012.762451 - link do publikacji
  4. Two-variable Logic with Counting and Trees
    Autorzy:
    Witold Charatonik, Piotr Witkowski
    Czasopismo:
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC (rok: 2016, tom: 17(4), strony: 31:1-31:27), Wydawca: ACM
    Status:
    Opublikowana
    Doi:
    10.1145/2983622 - link do publikacji
  5. Theorem Proving for Classical Logic with Partial Functions by Reduction to Kleene Logic
    Autorzy:
    Hans de Nivelle
    Czasopismo:
    Journal of Logic and Computation (rok: 2017, tom: 27(2), strony: 509-548), Wydawca: Oxford University Press
    Status:
    Opublikowana
    Doi:
    10.1093/logcom/exu071 - link do publikacji
  6. Two-variable Logic with Counting and a Linear Order
    Autorzy:
    Witold Charatonik, Piotr Witkowski
    Czasopismo:
    Logical Methods in Computer Science (rok: 2016, tom: 12(2:8), strony: 45322), Wydawca: LOGICAL METHODS IN COMPUTER SCIENCE e.V.
    Status:
    Opublikowana
    Doi:
    10.2168/LMCS-12(2:8)2016 - link do publikacji
  1. Subsumption Algorithms for Three-Valued Geometric Resolution
    Autorzy:
    Hans de Nivelle
    Konferencja:
    International Joint Conference on Automated Reasoning (IJCAR) 2016 (rok: 2016, ), Wydawca: Springer International Pulblishing
    Data:
    konferencja 27 czerwca - 2 lipca 2016
    Status:
    Opublikowana
  2. Decidability of weak logics with deterministic transitive closure
    Autorzy:
    Witold Charatonik, Emanuel Kieroński, Filip Mazowiecki
    Konferencja:
    Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (rok: 2014, ), Wydawca: ACM
    Data:
    konferencja 14-18 lipca 2014
    Status:
    Opublikowana
  3. Complexity of Two-Variable Logic on Finite Trees
    Autorzy:
    Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, James Worrell
    Konferencja:
    Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013 (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja July 8-12
    Status:
    Opublikowana
  4. Theorem Proving for Logic with Partial Functions by Reduction to Kleene Logic
    Autorzy:
    Hans de Nivelle
    Konferencja:
    Automated Reasoning in Quantified Non-Classical Logics ARQNL 2014 (rok: 2014, ), Wydawca: VSL Workshop Proceedings
    Data:
    konferencja 23 lipca 2014
    Status:
    Opublikowana
  5. Two-Variable Logic with Counting and Trees
    Autorzy:
    Witold Charatonik, Piotr Witkowski
    Konferencja:
    28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 (rok: 2013, ), Wydawca: IEEE Computer Society
    Data:
    konferencja June 25-28
    Status:
    Opublikowana