BCI logic, Clause Evaluation, contraction-free logics, Graph Neural Networks, local deduction theorems, machine learning, theorem proving.