abella-reasoning Formalization of the cut-elimination theorem for linear logic related proof systems using Abella, a proof assistant based on lambda-tree syntax.