Projects funded by the NCN

Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Decision procedures in verification

2011/03/B/ST6/00346

Keywords:

decision problem verification logic automated theorem proving

Descriptors:

  • ST6_7: Artificial intelligence, intelligent systems, multi-agent systems
  • ST1_1: Logic and foundations

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Uniwersytet Wrocławski, Wydział Matematyki i Informatyki

woj. dolnośląskie

Other projects carried out by the institution 

Principal investigator (from the host institution):

prof. Witold Charatonik 

Number of co-investigators in the project: 5

Call: OPUS 2 - announced on 2011-09-15

Amount awarded: 483 450 PLN

Project start date (Y-m-d): 2012-08-31

Project end date (Y-m-d): 2016-02-29

Project duration:: 42 months (the same as in the proposal)

Project status: Project settled

Equipment purchased [PL]

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

Information in the final report

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

O Narodowym Centrum Nauki

Finansowanie nauki

Współpraca zagraniczna

Centrum prasowe

Deklaracja dostępności
Przetwarzanie danych osobowych
Polityka cookies

Partnerzy