Coherence via focusing for symmetric skew monoidal and symmetric skew closed categoriesVeltri, NiccoloJournal of logic and computation2024 / art. exae059, 26 phttps://doi.org/10.1093/logcom/exae059
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