No label defined (Q4815865)

The authors consider a tableau system for propositional BCK logic (a substructural logic characterized by omitting the structural rule of contraction). Signed formulae in the propositional language with the unary connective \(\neg\) and the binary connectives \(\wedge\), \(\cdot\), \(\vee\), \(+\), \(\rightarrow\), \(-\!\circ\) (the absence of contraction has split the usual binary connectives into distinct pairs) are divided into four classes, and reduction rules according to these classes, are given. For the definitions and results necessary to understand this tableau system, one should consult the second author's unpublished paper: ``Tableaux for substructural logics''. The second part is devoted to an algorithm for theorem proving in BCK logic based on the system developed in the first part. For the entire collection see [Zbl 1011.00025].