Algorithm for proving in intuitionistic propositional logic with limited number of atoms

Na mocy twierdzenia Diego, które mówi o skończoności algebraicznego modelu wolnego dla minimalnej logiki zdaniowej, oraz jego uszczegółowień szacujących rozmiar tego modelu wiadomo, że istnieje wielomianowy algorytm rozstrzygający prawdziwość formuł minimalnej logiki zdaniowej przy założeniu, że liczba dostępnych atomów zdaniowych jest ograniczona. Jednak naiwny algorytm wymaga pozyskania tablicy reprezentującej klasy abstrakcji formuł tej logiki zdaniowej, a ta jest bardzo dużych rozmiarów. Fakt ten czyni zadanie zapisania tego algorytmu w praktyce niewykonalnym. W trakcie referatu przedstawiony zostanie inny wielomianowy algorytm dla tego problemu, oparty na teoriodowodowych obserwacjach.

Diego theorem, that gives finiteness of algebraic free model of minimal propositional logic, together with its enhancements that estimate the number of model's elements we know that there is a polynomial time algorithm that decides validity of formulas in minimal propositional logic, assuming that the number of available propositional atoms is limited. However the naive algorithm requires a table that represents abstraction classes of this propositional logic and the table is of big size. This circumstance makes the task of writing down the algorithm intractable. In this talk an alternative algorithm will be presented that is based upon proof-theoretic observations.