A resolution-based decision procedure for extensions of K4The two-variable guarded fragment with transitive relations
