Матричный способ записи сетей меток

В заметке приводится упрощенный вариант принадлежащего автору метода установления выводимости в интуиционистском исчислении высказываний (ИИВ). Проверяемая на выводимость формула сначала преобразуется в конъюнкцию $\pi$-цепей [I]. Затем каждая $\pi$-цепь переписывается в виде матрицы. После этого некоторые вхождения атомарных формул отмечаются знаками “+” или “-” по так называемому “правилу меток”. Вводится понятие законченной матрицы. Основным результатом является следующая теорема: выводимость $\pi$-цепи в ИИВ равносильна возможности построить для этой $\pi$-цепи законченную матрицу.