de Nivelle, H., & Kazakov, Y.(2004). Resolution decision procedures for the guarded fragment with transitive guards (MPI-I-2004-2-001). Saarbrücken: Max-Planck-Institut für Informatik.