James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the Association for Computing Machinery, vol. 14 (1967), pp. 687–697.
Keyword(s):