Sequent calculus for nonmonotonic/defeasible logics? 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.
There is a paper by Beyersdorff and Chew on the proof complexity of calculi for non-monotonic logic. In the references of this paper you will find links to the papers where these calculi are defined.