Non-Equivalence of Some Implicational Deduction Theorems

Abstract

We show that some classes of logics in the hierarchy of Implicational Deduction Theorems, defined in the forthcoming paper by Chvalovský and Cintula, are not equal. This completes the picture of hierarchy of these logics.

Keywords

• implicational deduction theorems
• contraction-free logics
• automated theorem proving