Gröbner bases in universal enveloping algebras of Leibniz algebras

We give a proof of the Poincaré–Birkhoff–Witt theorem for universal enveloping algebras of finite dimensional Leibniz algebras using Gröbner bases in a free associative algebra.We also construct Gröbner bases for two-sided ideals in universal enveloping algebras using the concept of Factor-Gröbner basis introduced by Nordbeck [Nordbeck, P., 2001. On the finiteness of Gröbner bases computation in quotients of the free algebra. Appl. Algebra Engrg. Comm. Comput. 11, 157–180]. Our approach differs from the one applied to PBW algebras or G-algebras since our algebras have zero divisors. We use this technique to obtain an algorithm to solve the ideal membership problem.