Znaczenie pojęcia odrzucania we współczesnej logice^[1]

Głównym celem artykułu jest pokazanie, w jaki sposób pojęcie odrzucania było rozwijane w ciągu ostatnich kilkunastu lat i jaką rolę pełni obecnie w logice. Pojęcie odrzucania zostało wcześniej poddane wnikliwej analizie przez szkołę opolską skoncentrowaną wokół Jerzego Słupeckiego. Od tego czasu ukazały się interesujące artykuły, które rzucają nowe światło na tę problematykę. Celem artykułu nie jest dostarczenie pełnego przeglądu ewolucji badań nad systemami odrzucania w logice, lecz jedynie zwrócenie uwagi na pewne interesujące wyniki.

W pierwszej części artykułu zarysowana zostaje historia pojęcia odrzucania. W drugiej części przedstawiono najistotniejsze powody, dla których warto badać systemy odrzucania. Trzecia część artykułu dotyczy zastosowań reguł odrzucania. W tej części przybliżone zostają najważniejsze założenia mieszanego systemu aksjomatycznego dla Bi-intuicjonistycznej logiki zaproponowanego przez Rajeeva Goré i Lindę Postniece^[2]. Następnie pokazano zastosowanie odrzucania przez Camilla Fiorentiniego do stworzenia procedury decyzyjnej dla logiki S4^[3]. Jako ostatni przykład opisano zastosowanie odrzucania (w węższym znaczeniu tego pojęcia) przez George'a Weissenbachera do znajdowania interpolantów^[4].

1. Historia pojęcia odrzucania na gruncie logiki formalnej

Pojęcie odrzucania zostało wprowadzone do logiki formalnej przez Jana Łukasiewicza. W swojej pracy poświęconej badaniu sylogistyki Arystotelesa Łukasiewicz zwrócił uwagę na fakt, że spośród dwóch aktów intelektualnych (uznawania oraz odrzucania zdań), jedynie idea uznawania była należycie badana na gruncie logiki^[5]. Wyraża ona oczywiste przeświadczenie, że zdania prawdziwe muszą być uznawane. Analogicznie, zdania fałszywe należy odrzucić. Łukasiewicz zwrócił uwagę, że również inne poprawne wyrażenia systemu logicznego np. funkcje zdaniowe, które nie są ani prawdziwe, ani fałszywe, powinny być odrzucone. Najprawdopodobniej Arystoteles zdawał sobie sprawę z tego faktu, gdyż odrzucił większość niepoprawnych form sylogistycznych wskazując na konkretne terminy, które je obalały. Takie podejście jest jednak niewłaściwe z perspektywy logiki formalnej, dlatego też Łukasiewicz zaproponował, aby odrzucić wszystkie niepoprawne formy sylogistyczne przez zastosowanie reguł odrzucania do figur odrzuconych aksjomatycznie. Skonstruowany w ten sposób pierwszy system odrzucania składał się z dwóch aksjomatów oraz dwóch reguł:

1. a) reguły odrzucania przez odrywanie: „Jeśli została uznana implikacja »Jeśli α, to β«, lecz został odrzucony jej następnik β, to jej poprzednik α także musi być odrzucony”^[6].
2. b) reguły odrzucania przez podstawienie: „Jeśli β jest podstawieniem α, i β zostało odrzucone, to α także musi być odrzucone”^[7].

Na gruncie tego systemu można obalić wszystkie niepoprawne tryby sylogistyczne, a na gruncie systemu aksjomatycznego można uznać wszystkie formuły logicznie prawdziwe. Słupecki udowodnił jednak, że dodatkowo istnieje nieskończenie wiele wyrażeń sensownych, o których nie można rozstrzygnąć na gruncie zaproponowanych systemów, czy są prawdziwe czy fałszywe. Dopiero uzupełnienie systemu odrzucania o regułę Słupeckiego uczyniło sylogistykę Arystotelesa rozstrzygalną z perspektywy logiki formalnej. Sens tej reguły jest następujący:

Jeśli γ nie wynika ani z α, ani z β, to nie może też wynikać z ich koniunkcji, ponieważ niczego, co nie wynika z dwóch przesłanek przeczących wziętych z osobna, nie można wyprowadzić z ich koniunkcji^[8].

Systemy odrzucania stały się następnie przedmiotem badań przede wszystkim logików związanych ze Słupeckim. Do najciekawszych wyników w tym czasie można zaliczyć pracę Słupeckiego, Brylla i Wybraniec-Skardowskiej The Theory of Rejected Propositions^[9], w której dokonano badań na gruncie metodologii nauk empirycznych. Wykorzystując zarówno pojęcie uznawania, jak i odrzucania, scharakteryzowano, czym jest: zdanie empiryczne, hipoteza, uogólnienie oraz wnioskowanie indukcyjne. Dzięki przeprowadzonej analizie autorzy doszli do wniosku, że systemy nauk empirycznych mają podstawowe własności takie same jak systemy nauk dedukcyjnych. Grzegorz Bryll zebrał większość osiągnięć grupy skoncentrowanej wokół Słupeckiego w monografii Metody odrzucania wyrażeń^[10]. Dokładnej analizie w tej monografii poddano między innymi pojęcie konsekwencji logicznej w kontekście odrzucania. Bryll zebrał również najważniejsze wyniki związane z aksjomatycznym odrzucaniem wyrażeń^[11], a także opisał uogólnioną metodę dedukcji naturalnej, w której oprócz reguł uznawania wyrażeń stosuje się też reguły ich odrzucania. W tej metodzie dowody mają postać drzew, których gałęzie tworzy się według zasady koniunkcyjnej lub zasady alternatywnej. Jedyną regułą dowodzenia jest reguła tworzenia dowodu nie wprost. Ponadto przyjmuje się założenie, że zbiór aksjomatów uznanych i zbiór aksjomatów odrzuconych są zbiorami pustymi^[12]. Jest to metoda podobna do tzw. tablic semantycznych. Podobne rozwiązanie rozwinął w swojej pracy doktorskiej Rafał Dutkiewicz^[13].

Na Zachodzie pojęcie odrzucania było badane przez takich myślicieli jak Rudolf Carnap, Georg Kreisel czy Hilary Putnam. Zajmowali się oni między innymi problemem znalezienia charakterystycznego systemu odrzucania dla logiki intuicjonistycznej. Rozwiązanie tego problemu przedstawił Dana Scott^[14], opisując nieskończoną rodzinę niestrukturalnych reguł, które dodane do klasycznego systemu odrzucania Łukasiewicza stworzyły kompletny system odrzucania dla logiki intuicjonistycznej. Ponadto Scott wprowadził bardzo prostą metodę udowadniania syntaktycznej zupełności systemu. Metoda wypracowana przez Scotta została następnie z powodzeniem zaadaptowana przez Tomasza Skurę, który wypracował ogólną metodę otrzymywania aksjomatycznych systemów odrzucania^[15]. Metoda ta składa się z następujących kroków:

1. a) Użycia procedury redukującej dowolną formułę do postaci normalnej.
2. b) Otrzymania reguły R, którą można zastosować do postaci normalnej. Ta reguła wraz z klasycznym systemem odrzucania pozwala na odrzucanie wyrażeń.
3. c) Pokazania, że każda postać normalna posiada albo dowód, albo odrzucenie.
4. d) Sprawdzenia, czy reguła R jest poprawna.

Podsumowując, początkowo zaniedbane pojęcie odrzucania stało się przedmiotem rzetelnych badań.

2. Dlaczego systemy odrzucania są ważne?

Istnieje wiele powodów, dla których warto badać systemy odrzucania. Po pierwsze, jak pokazano w pierwszej części artykułu, reguły odrzucania mają znaczenie przy badaniu rozstrzygalności rachunków logicznych. Z formalnego punktu widzenia rozstrzygalność można badać niejako od dwóch stron. Systemy aksjomatyczne dla uznanych wyrażeń pozwalają na skonstruowanie dowodów tylko dla formuł, które są tezami, a więc na mocy twierdzenia o pełności są one tautologiami^[16]. Jeżeli jakiejś formuły nie można dowieść na gruncie takiego systemu, oznacza to, że albo nie potrafimy skonstruować dla niej dowodu (ponieważ nasze narzędzia formalne są niewystarczające, np. procedura jest niewykonywalna w realnym czasie), albo nie jest ona tezą, a więc należy ją odrzucić. Analogicznie formuły mające dowód na gruncie systemu odrzucania (czyli wyprowadzone z aksjomatycznie odrzuconych wyrażeń za pomocą reguł odrzucania) nie są tezami, czyli nie są też tautologiami. Jeżeli jakaś formuła nie może zostać odrzucona na gruncie systemu odrzucania, to oznacza, że albo nie umiemy skonstruować dla niej odrzucenia, albo jest tezą, a więc i tautologią. Ta symetria sprawia, że w ogólności oba podejścia są tak samo zasadne. Ale przy rozważaniu poszczególnych logik mogą pojawić się różnice. Na przykład Skura skonstruował bardzo użyteczny system odrzucania na gruncie klasycznej logiki zdaniowej pozwalający na rozstrzygnięcie, czy dla danej formuły istnieje odrzucenie, czy też dowód^[17]. System ten charakteryzuje się tym, że wszystkie reguły odrzucania są odwracalne oraz każda z ich przesłanek jest prostsza od wniosku. Dzięki temu procedura rozstrzygania, czy dane wyrażenie jest tezą czy nią nie jest, opiera się na pewnego rodzaju redukcji i jest wolna od powtórzeń charakterystycznych między innymi dla metody tablic Betha zastosowanej dla klasycznej logiki zdaniowej. Podsumowując, systemy odrzucania pozwalają nie tylko teoretycznie rozwiązać problem rozstrzygalności (przez umożliwienie skonstruowania listy nie-praw), ale również są jednym z praktycznych narzędzi rozstrzygania czy dana formuła jest prawem logicznym, czy nim nie jest^[18].

Po drugie, bardzo często na bazie syntaktycznego odrzucania można skonstruować semantyczne odrzucenie, dzięki czemu systemy odrzucania mogą być użyteczne przy konstruowaniu modeli i kontrmodeli. Przez model rozumiane jest takie Boole'owskie wartościowanie, które każdej zmiennej zdaniowej przyporządkowuje wartość 1 lub 0 i które jest rozszerzone na złożone formuły za pomocą reguł właściwych dla danej logiki. Dane wartościowanie jest nazywane kontrmodelem dla pewnej formuły A, gdy wartość przypisana tej formule zgodnie z regułami obowiązującymi dla danej logiki wynosi 0. W pracy What is a refutation system?^[19]. Skura poddał analizie relację systemów odrzucania do tzw. standardowych metod (czyli modeli i tablic), w których odrzucenie jest znajdowane w pośredni sposób (jako porażka w próbie uznania sprawdzanej formuły). W swoim artykule Skura doszedł do wniosku, że każde odrzucenie determinuje pewien kontrmodel, a każdy kontrmodel określa pewne odrzucenie. Skura przedstawił dowód tego twierdzenia, który jednak nie będzie przytaczany w tym artykule (zainteresowanych czytelników odsyłam do wspomnianej wyżej pracy). W innych pracach Skura pokazał również, jak na bazie syntaktycznego odrzucania skonstruować modele na przykład dla logiki klasycznej^[20] oraz dla logiki modalnej K4^[21].

Po trzecie, niektóre z reguł odrzucania są regułami hybrydowymi tzn. składają się zarówno z części, w której uznaje się jakąś przesłankę (np. implikację „Jeśli α, to β”), jak i z części w której odrzuca się inną przesłankę (np. następnik β), i dopiero kombinacja tych dwóch przesłanek pozwala na odrzucenie wniosku (np. poprzednika α). Taką postać ma między innymi reguła odrzucania przez odrywanie (nazywana odwrotnym modus ponens), która została zaproponowana przez Łukasiewicza. Valentin Goranko zwrócił uwagę na fakt, że po zaakceptowaniu istnienia takich reguł naturalne jest rozpoczęcie badań nad hybrydowymi regułami uznawania, czyli takimi których przesłanki byłyby zarówno uznawane, jak i odrzucane, a wniosek byłby uznany^[22]. Takie podejście jest bardzo ciekawe z filozoficznego punktu widzenia, ponieważ otwiera nowe perspektywy badania zależności pomiędzy uznawaniem i odrzucaniem na poziomie metalogicznym. Goranko zwraca uwagę, że połączenie pojęć uznawania i odrzucania pozwala w prosty sposób wyrazić takie pojęcia metalogiczne, jak niesprzeczność czy pełność systemu logicznego. Goranko przedstawił też możliwe korzyści, jakie przyniesie rozwijanie łączonych systemów dedukcji na gruncie nauk komputerowych. Z filozoficznej perspektywy bardziej interesujący wydaje się wpływ, jaki takie podejście będzie miało na przykład na gruncie badań nad językiem naturalnym. Już Arystoteles zauważył, że racjonalna dyskusja podlega pewnym regułom. W sytuacji kiedy dyskutant chce podważyć stanowisko swojego adwersarza, może to zrobić na dwa sposoby: albo udowodnić tezę przeciwną, albo wykazać błędność rozumowania swojego rozmówcy, czyli odrzucić jego wnioskowanie.

3. Przykłady zastosowania reguł odrzucania

W tej części artykułu zaprezentowane zostaną trzy zastosowania reguł odrzucania. Pierwsze z nich wiąże się ze skonstruowaniem przez Rajeeva Goré i Lindę Postniece mieszanego rachunku sekwentów. Drugie dotyczy skonstruowania przez Fiorentiniego algorytmu szukania dowodu lub odrzucenia dla danego sekwentu dla logiki modalnej S4. Trzecie pokazuje, w jaki sposób odrzucanie (w wąskim znaczeniu tego słowa) jest wykorzystane do znajdowania interpolantów^[23], co ma szczególne zastosowanie w automatycznej weryfikacji oprogramowania.

W artykule Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic Goré i Postniece zaprezentowali aksjomatyczny system sekwentów^[24], w którym występuje zarówno uznawanie, jak i odrzucanie wyrażeń^[25]. Systemy odrzucania (zachowujące własność bycia nie-prawem) były do tej pory badane jako odrębne systemy aksjomatyczne, komplementarne w stosunku do systemów aksjomatycznych zachowujących własność bycia prawem. Na przykład rachunek CRIP (Calculus for Refutation of Intuitionistic Propositions) zaproponowany przez Pinto i Dyckhoffa jest dopełnieniem systemu aksjomatycznego LJT* dla IPL (Intuitionistic Propositional Logic)^[26]. Razem pozwalają one w prosty sposób pokazać, że dla dowolnego sekwentu istnieje albo dowód (na mocy systemu LJT*), albo odrzucenie (na mocy systemu CRIP), ale nigdy oba naraz.

Jak wspomniano w części II artykułu, Goranko zwrócił uwagę na fakt, że niektóre reguły odrzucania mają hybrydowy charakter, a badanie wzajemnych związków między uznaniem i odrzucaniem w ramach jednego systemu może przynieść bardzo ciekawe wyniki. Praca Rajeeva Goré i Lindy Postniece faktycznie pokazuje potencjał tkwiący w systemach tego typu. Podstawowymi pojęciami tego systemu są: sekwent oraz antysekwent. Sekwent rozumiany jest w tradycyjny sposób, tzn. jest on logicznie prawdziwy (w modelu), gdy spełniony jest następujący warunek: jeśli wszystkie elementy zbioru poprzedników są prawdziwe, to przynajmniej jeden element ze zbioru następników jest prawdziwy. Antysekwent zdefiniowany jest następująco: istnieje taki model, w którym wszystkie elementy zbioru poprzedników są prawdziwe, a wszystkie elementy ze zbioru następników są fałszywe. Wykorzystując te pojęcia Goré i Postniece oparli swój system na trzech aksjomatach oraz jednym antyaksjomacie. Podczas konstruowania dowodów na gruncie tego systemu własność bycia sekwentem lub antysekwentem jest przenoszona w dół drzewa (aż do korzenia) za pomocą wprowadzonych reguł. Otrzymujemy wyprowadzenie dla danego sekwentu, gdy korzeń jest sekwentem w tradycyjnym ujęciu, a odrzucenie, gdy korzeń jest antysekwentem. Reguły zaproponowane przez Rajeeva Goré i Lindę Postniece mają charakter hybrydowy, na przykład reguła dotycząca występowania koniunkcji formuł po prawej stronie sekwentu może mieć następujące cztery formy:

1. 1) obie przesłanki są sekwentami i wniosek też jest sekwentem;
2. 2) pierwsza przesłanka jest sekwentem, druga jest antysekwentem, a wniosek jest antysekwentem;
3. 3) pierwsza przesłanka jest antysekwentem, druga jest sekwentem, a wniosek jest antysekwentem.
4. 4) obie przesłanki są antysekwentami i wniosek też jest antysekwentem.

Przedstawione wyżej formy nie wyczerpują jednak wszystkich możliwych kombinacji pomiędzy uznawaniem i odrzucaniem wyrażeń. Goré i Postniece pokazują, że w pewnych szczególnych przypadkach można z sekwentu i antysekwentu jako przesłanek otrzymać sekwent jako wniosek. Ponadto skonstruowany w ten sposób system ma konkretne zastosowanie praktyczne. Łatwo na jego gruncie stworzyć procedurę rozstrzygającą dla dowolnego sekwentu, czy ma on zostać uznany czy odrzucony, co pozwala jednocześnie automatycznie stworzyć odpowiadające mu drzewo.

Goré i Postniece zwracają uwagę, że chociaż złożoność obliczeniowa zaproponowanej przez nich metody rozstrzygania dla logiki Bi-intuicjonistycznej wynosi O(2^m), to posiada ona cechy wyróżniające ją na tle tradycyjnych metod. Przede wszystkim wyraża ona pewne intuicje metalogiczne związane z pojęciami uznania i odrzucania wyrażeń. Ponadto w prosty sposób pozwala otrzymać nie tylko klasyczny dowód pełności, ale również pokazać pełność dla wyrażeń odrzuconych. Wydaje się, że dalsze badanie rachunków tego typu z pewnością przyniesie korzyści zarówno pod względem teoretycznym, jak i praktycznym.

Fiorentini w artykule Terminating sequent calculi for proving and refuting formulas in S4 przedstawił dwa rachunki sekwentów dla logiki modalnej S4: GS4 zachowujący własność bycia prawem oraz RS4 zachowujący własność bycia nie-prawem^[27]. Oba rachunki posiadają dwie kluczowe własności: po pierwsze występujące w nich reguły są malejące tzn. po zastosowaniu reguły do danego sekwentu otrzymany sekwent jest prostszy, po drugie reguły zachowują słabą własność podformuły, tzn. sekwenty otrzymane po zastosowaniu reguł do danego sekwentu są zbudowane tylko z formuł występujących w tym sekwencie. Własności te wynikają z rozszerzenia przez Fiorentiniego języka logiki S4 o dwa nowe spójniki modalne. Dodatkowo Fiorentini zastosował reguły uznawania (dla GS4) oraz odrzucania (dla RS4) do postaci normalnych w stylu Mintsa^[28], zwrócił jednak uwagę na fakt, że takie podejście nie zmniejsza ogólności jego rozważań, ponieważ dowolny sekwent może zostać sprowadzony do postaci normalnej. Jedna z takich procedur opisana jest w Appendiksie A do wspomnianego artykułu. Wykorzystując rachunki GS4 oraz RS4 Fiorentini skonstruował algorytm pozwalający dla danego sekwentu (w postaci normalnej) otrzymać albo dowód (w GS4), albo odrzucenie (w RS4). Zaproponowana przez niego procedura jest skończona oraz bardzo efektywna, dzięki wykorzystaniu dodatkowych spójników rozszerzających język logiki S4.

Podsumowując, poszukiwanie dowodów dla logiki S4 nie jest łatwe ze względu na relację przechodniości, która doprowadza do wystąpienia nieskończonych sekwencji w dowodzie. Metodą najczęściej stosowaną do obejścia tego problemu jest tzw. „loop-checking”, który polega na tym, że po wystąpieniu tego samego sekwentu dwa razy na danej gałęzi szukanie dowodu jest przerywane. Wykorzystując rachunki GS4 oraz RS4, dzięki posiadaniu malejących reguł oraz zachowywaniu słabej własności podformuły, Fiorentini rozwiązał ten problem w prostszy i bardziej intuicyjny sposób, otrzymując elegancką procedurę decyzyjną dla logiki S4.

Trzecim przykładem zastosowania odrzucania jest wykorzystywanie reguł odrzucania na gruncie nauk komputerowych. W literaturze pojęcie odrzucania wykorzystywane jest również w węższym znaczeniu, niż przedstawione w tym artykule, jako wyprowadzenie fałszu. W takim sensie jest ono użyte na przykład przez Weissenbachera. W swojej pracy doktorskiej Weissenbacher zwrócił szczególną uwagę na rolę odrzucania w znajdowaniu interpolantów, co jest wykorzystywane w jednej z metod automatycznej weryfikacji oprogramowania. Użyteczność interpolantów w tej dziedzinie została zauważona dopiero niedawno, ale jest ona obecnie bardzo rozwijana. Oprócz znajdowania interpolantów bardzo istotne jest też znajdowanie kontrprzykładów, co pozwala na identyfikację błędów w programach, które negatywnie przeszły weryfikację. W swojej pracy Weissenbacher przedstawia nową technikę znajdowania interpolantów z dowodów odrzucania, która od wcześniejszych metod różni się tym, że pozwala na otrzymanie wielu interpolantów dla danej formuły. Jednocześnie pozwala ona na określenie siły otrzymanych interpolantów. Ogólnie metoda ta opiera się na wykorzystaniu alternatywnego sformułowania twierdzenia Craiga (nazywanego twierdzeniem Craiga-Robinsona), zgodnie z którym:

Jeśli A i B są zamkniętymi formułami logiki kwantyfikatorów oraz z koniunkcji A i B wynika fałsz, to wówczas istnieje taka zamknięta formuła I, że z formuły A wynika formuła I, a z formuły B wynika negacja formuły I, zaś wszystkie funkcje i predykaty występujące w formule I występują zarówno w formule A, jak i w B^[29].

Otrzymany w ten sposób interpolant często jest nazywany „odwrotnym interpolantem”, ponieważ jest to faktycznie interpolant dla formuły A oraz negacji formuły B. Wykorzystując alternatywne sformułowanie twierdzenia Craiga można dla danej pary formuł A i B otrzymać interpolant z dowodu odrzucania dla koniunkcji formuły A oraz negacji formuły B^[30]. Laura Kovács i Andrei Voronkov pokazali, że taka procedura może zostać wykonana w liniowym czasie, jeśli każde wnioskowanie w dowodzie jest lokalne^[31]. Wnioskowanie nazywamy lokalnym ze względu na formuły A i B, jeśli spełnione są następujące warunki:

1. (i) albo przesłanki i wniosek są podzbiorem języka formuły A, albo przesłanki i wniosek są podzbiorem języka formuły B;
2. (ii) jeśli wszystkie przesłanki wnioskowania zawierają jedynie zmienne wspólne dla formuł A i B, to wniosek również zawiera wyłącznie zmienne wspólne dla formuł A i B^[32].

Weissenbacher w swojej pracy zaadoptował to podejście do znajdowania interpolantów na gruncie bit-wektorowej arytmetyki^[33]. Dzięki temu mógł tę metodę wykorzystać w procedurze automatycznej weryfikacji oprogramowania. Przykład ten pokazuje, że odrzucanie jest użyteczne również na gruncie nauk komputerowych.

4. Podsumowanie

Na początku XX wieku pojęcie odrzucania nie było badane ani pod kątem teoretycznych, ani praktycznych zastosowań. Pierwsze poważne badania rozpoczęli Łukasiewicz, Słupecki oraz ich uczniowie. Po wnikliwej analizie na gruncie teoretycznym odrzucanie zaczęto postrzegać jako uzupełnienie uznawania. Kolejne badania pokazały potencjał płynący z możliwości alternatywnego opisania części pozytywnej systemu logicznego. Przede wszystkim zaowocowało to eleganckim udowodnieniem pełności wielu systemów logicznych oraz możliwością skonstruowania prostych procedur rozstrzygania czy dana formuła jest prawem, czy jest nie-prawem.

W latach 90. coraz częściej pojęcie odrzucania stosowane jest w celu rozwiązywania konkretnych problemów na gruncie logiki. Goranko zwrócił uwagę na potencjał tkwiący w analizie reguł hybrydowych wykorzystujących zarówno odrzucanie jak i uznawanie przesłanek. W sposób praktyczny podejście to zostało wykorzystane przez Rajeeva Goré i Lindę Postniece do skonstruowania mieszanego systemu aksjomatycznego dla logiki Bi-intuicjonistycznej.

W latach 90. zaczęto również konstruować coraz liczniejsze uzupełniające się rachunki uznawania oraz rachunki odrzucania. Przykładem takiego systemu jest rachunek odrzucania CRIP skonstruowany przez Pinto i Dyckhoffa, który jest dopełnieniem aksjomatycznego systemu dla logiki intuicjonistycznej. Obecnie takie podejście jest nadal rozwijane. Jednym z przykładów jest praca Fiorentiniego, w której opisał dwa uzupełniające się rachunki sekwentów: GS4 oraz RS4. Dzięki wprowadzeniu dodatkowych spójników modalnych Fiorentini stworzył efektywny algorytm pozwalający w skończonym czasie dla danego sekwentu logiki modalnej S4 otrzymać albo dowód, albo odrzucenie (odrzucenie nie jest porażką w znalezieniu dowodu i dowód nie jest porażką w znalezieniu odrzucenia).

Oprócz wyraźnych zastosowań na gruncie czystej logiki, pojęcie odrzucania jest użyteczne również w innych dziedzinach naukowych w tym na gruncie nauk komputerowych. Przykładem może być rola odrzucania (w węższym znaczeniu tego pojęcia) w metodzie znajdowania interpolantów z dowodów odrzucania przez stosowanie reguły rezolucji. Weissenbacher pokazał, że metoda ta jest bardzo skuteczna na gruncie arytmetyki bit-wektorowej do znajdowania wielu interpolantów dla zadanej pary formuł.