Completeness of resolution for definite answersTammet, TanelJournal of logic and computation1995 / 4, p. 449-471
Optimized encodings of fragments of type theory in first-order logicTammet, Tanel; Smith, Jan M.Journal of logic and computation1998 / 6, p. 713-744https://www.cse.chalmers.se/~smith/autolncs.pdf