Is it possible to construct sequent calculus for nonmonotonic/defeasible logic? If it is possible then those logics can be encoded in proof assistants which require sequent calculus for logic to be encoded (Isabelle, Coq).
I am aware of the several papers from the late nineties by Ana Teresa Martins et al. about sequent calculus for paraconsistent logics. the labelling of propositions (given and derived) is used in those papers. But those papers seems to be unpublished, although they contain bright ideas, the quality of language may be a bit higher. It seems to me that those ideas are not caught by others and developed futher.