Abstract:

An O(n log n)-space decision procedure for the relevance logic B+

Luca Viganò


In previous work we gave a new proof-theoretical method for establishing upper-bounds on the space complexity 
of the provability problem of modal and other propositional non-classical logics. Here we extend and refine these 
results to give an O(n log n) decision procedure for the basic positive relevance logic B+. We compute this 
upper-bound by first giving a sound and complete, cut-free, labelled sequent system for B+, and then establishing
bounds on the application of the rules of this system.