Nauka i badania

Prowadzę badania w zakresie logik substrukturalnych, a w szczególności rozszerzeń niełącznego rachunku Lambeka. Szczególnie interesują mnie te rozszerzenia, które stanowią osłabienia logiki liniowej.

Niełączna logika biliniowa

Niełączna logika biliniowa to multiplikatywno-addytywna logika liniowa Girarda bez założenia łączności i przemienności produktu (koniunkcji multiplikatywnej). Dla tej logiki udało mi się pokazać lewostronny system sekwentowy, który ma własność eliminacji cięć. W konsekwencji można łatwo uzyskać z niego system prawostronny.

Dla multiplikatywnego fragmentu tej logiki (tj. bez spójników i stałych addytywnych) udowodniłem, że czysta logika jest rozstrzygalna w czasie wielomianowym.

Problemem otwartym pozostaje rozstrzygalność relacji konsekwencji dla tej logiki.

Cykliczna niełączna logika biliniowa

Cykliczna niełączna logika biliniowa to niełączna logika biliniowa z dodatkowym założeniem, że negacje liniowe są sobie równe (tzn. mamy jedną negację spełniającą prawo podwójnej negacji). Dla tej logiki również wskazałem system sekwentowy lewostronny z własnością eliminacji cięć.

Pokazałem, że logika ta jest silnie zachowawczym rozszerzeniem pełnego niełącznego rachunku Lambeka (bez stałych addytywnych). Twierdzenie to zachodzi zarówno dla wariantu ze stałymi multiplikatywnymi jak i bez nich. Co więcej, przeniosłem ten wynik na warianty łączne. W konsekwencji te same twierdzenia zachodzą dla wersji niecyklicznej.

Opublikowałem konstruktywny dowód tego faktu dla logiki niełącznej, podając ciekawy system, w którym założenia pozalogiczne nie są aksjomatami, a regułami.

Boolowski i heytingowski pełny niełączny rachunek Lambeka

Boolowski pełny niełączny rachunek Lambeka to rozszerzenie dystrybutywnego pełnego niełącznego rachunku Lambeka o negację boolowską. Można o tej logice również myśleć jak o rozszerzeniu logiki klasycznej o niełączny rachunek Lambeka. Dla tej logiki udowodniłem, że finitarna relacja konsekwencji jest rozstrzygalna w czasie wykładniczym.

Na podstawie wyników Shkatova i Van Altena wnioskujemy, że finitarna relacja konsekwencji jest EXPTIME-zupełna, jeżeli nie dopuszczamy stałej multiplikatywnej.

Heytingowski pełny niełączny rachunek Lambeka to rozszerzenie dystrybutywnego pełnego niełącznego rachunku Lambeka o implikację intuicjonistyczną albo rozszerzenie logiki intuicjonistycznej o niełączny rachunek Lambeka. Dla tej logiki wykazałem to samo co wyżej.

Problemem otwartym pozostaje dolna granica złożoności dla wariantów z jedynką.