Nauka i badania

Cykliczna niełączna logika biliniowa (CyNBL) to kompromis między niełączną logiką liniową i niełączną logiką biliniową, w której z jednej strony produkt dalej jest niełączny, ale negacja jest tylko jedna i spełnia prawa De Morgana.

1. Dla CyNBL udało się opracować nietypowy, jednostronny system sekwentowy, w którym założenia (aksjomaty pozalogiczne) nie są wyrażone jako aksjomaty, ale specjalne przypadki reguły cięcia. W ten sposób możemy znacząco ograniczyć zakres stosowania reguły cięcia, co likwiduje typowe wyzwania związane z tą regułą. Dzięki temu zabiegowi udało się pokazać konstruktywny dowód, że CyNBL bez stałych addytywnych jest silnie zachowawczym rozszerzeniem FNL.

   • Sequent Systems for Consequence Relations of Cyclic Linear Logics 2024
2. Dowód faktu o silnej zachowawczości CyNBL nad FNL można również udowodnić prościej, ale niekoniecznie konstruktywnie, przy pomocy metod algebraicznych. Nowością jest tutaj zastosowanie kwantali dla logiki z niełącznym produktem.

   • Applying Quantales to Lambek Calculi with Cyclic Negation 2026
3. w opracowaniu

   Wykorzystując metodę z ograniczaniem reguł cięcia do założeń, można również pokazać, że CyNBL ze stałymi addytywnymi jest silnie zachowawczym rozszerzeniem FNL, o ile w FNL dopuścimy tylko jedną stałą addytywną - kres górny. Dopuszczenie kresu dolnego sprawia, że CyNBL nie jest nawet słabo zachowawczym rozszerzeniem FNL.

Pełny niełączny rachunek Lambeka (FNL), czyli rachunek Lambeka ze spójnikami addytywnymi (kratowymi) ma nierozstrzygalną relację konsekwencji, co czyni go mało użytecznym w zakresie np. lingwistyki matematycznej. Jednakże jego niezachowawcze rozszerzenie, czyli dystrybutywny pełny niełączny rachunek Lambeka (DFNL), w którym operatory kratowe spełniają zasadę rozdzielności, ma rozstrzygalną relację konsekwencji w czasie wykładniczym. W wersji bez stałej multiplikatywnej logika ta jest nawet EXPTIME-zupełna.

1. Jedną z ciekawych form myślenia o rachunku Lambeka jest traktowanie jego spójników jako modalności dwuargumentowych. W ten sposób można obrać inny punkt wyjścia: zamiast rozszerzać rachunek Lambeka o inne spójniki i stałe, to inną logikę rozszerzyć o modalności lambekowskie. W ten sposób można uzyskać boolowski pełny niełączny rachunek Lambeka (BFNL), czyli z jednej strony logikę klasyczną rozszerzoną o NL jak i DFNL z dodaną negacją boolowską. Dla tej logiki udało mi się udowodnić, że ma rozstrzygalną relację konsekwencji w czasie wykładniczym, podobnie jak DFNL.

   • Complexity of Nonassociative Lambek Calculus with Classical and Intuitionistic Logic 2026
   • Complexity of Nonassociative Lambek Calculus with classical logic 2024
2. Naturalną kontynuacją jest podjęcie tego samego zagadnienia dla innych rozszerzeń DFNL. Heytingowski pełny niełączny rachunek Lambeka (HFNL) to logika intuicjonistyczna rozszerzona o NL lub DFNL z implikacją intuicjonistyczną. Dla tej logiki złożoność relacji konsekwencji również jest wykładnicza.

   • Complexity of Nonassociative Lambek Calculus with Classical and Intuitionistic Logic 2026

Niełączna logika biliniowa to multiplikatywno-addytywna logika liniowa Girarda bez założenia łączności i przemienności produktu (koniunkcji multiplikatywnej). Jej szczególną cechą jest obecność dwóch inwolutywnych negacji, które można traktować jako negację lewo- i prawo-stronną.

1. Dla tej logiki udało się opracować jednostronny system sekwentowy, który jest znacznie prostszy i szybszy w badaniu niż klasyczne systemu dwustronne (np. intuicjonistyczne). System ten dopuszcza eliminację cięć.

   • One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity 2021
2. Część multiplikatywna tej logiki (czyli bez spójników i stałych addytywnych) jest rozstrzygalna w czasie wielomianowym. Rozszerza to poprzedni wynik Buszkowskiego, który wykazał ten fakt dla wersji bez stałych multiplikatywnych.

   • One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity 2021
3. w opracowaniu

   Ponadto, część multiplikatywna (zarówno ze stałymi multiplikatywnymi jak i bez nich) ma rozstrzygalną relację konsekwencji, również w czasie wielomianowym. Logika ze spójnikami addytywnymi ma nierozstrzygalną relację konsekwencji, ponieważ jest silnie zachowawczym rozszerzeniem FNL.