Abstrakt
We study the independence of axioms in Hilbert-style calculi for some propositional non-classical logics, especially for substructural and fuzzy logics, by automated theorem proving methods. The standard approach to solve these problems is encoding in first-order classical logic.
We discuss some theoretical as well as practical issues of this approach and present several results e.g. the complete solution for prominent fuzzy logics MTL (Monoidal T-norm based Logic) and Hajek's BL (Basic Logic).