Implementation of a cut−free sequent calculus for logics with adjoint modalities
Mehrnoosh Sadrzadeh · 2009
Sadrzadeh and Dyckhoff describe in [1] a cut-free sequent calculus for logics with adjoint pairs of modal operators. We give here a Prolog implementation of a decision procedure for this calculus and describe the simple mechanism for loop checking used to guarantee termination, which requires slight modification of some of the inference rules of the calculus.