A category-theoretic treatment of automated theorem proving