A note on the completeness of resolution without self-resolution
The note shows that self-resolution in resolution-based deduction systems can be omitted. The completeness of resolution is a consequence of the completeness of hyperresolution.
scientific article; zbMATH DE number 4099255