Automated proof construction in type theory using resolution
scientific article; zbMATH DE number 1901556