Zhang, G. Q. (1989) “PB-277 Literal resolution: A Simple Proof of Resolution Completeness”, DAIMI Report Series, 18(277). doi: 10.7146/dpb.v18i277.6654.