Nowadays standard in automated theorem proofs are algorithms based on resolution system. There were quite a few attempts to present algorithms based on natural deduction (which is stronger than resolution), however, it turned out that such algorithms were less efficient than resolution-based ones.
On the other hand, extended Frege systems are at least as strong as Frege systems (and hence natural deduction) and can possibly be even super-polynomially stronger. Hence, the question: are (were) there any attempts to create an algorithm for proof search in extended Frege systems or natural deduction augmented with extension rule?