Algorithmic proof methods and cut elimination for implicational logics. I: Modal implication
goal directed proof theory for nonclassical logics
scientific article; zbMATH DE number 1512006