A full formalization of SLD-resolution in the calculus of inductive constructions
scientific article; zbMATH DE number 1394793